Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-dcmulti.opb |
MD5SUM | 659e380dd1d6168ad99a794b3190043f |
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 wulflinc21 THE 2005-09-19 17:45:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2967 boxname=wulflinc21 idbench=623 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 659e380dd1d6168ad99a794b3190043f /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-dcmulti.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-dcmulti.opb IDLAUNCH: 2967 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 889704 kB Buffers: 32852 kB Cached: 84588 kB SwapCached: 812 kB Active: 63244 kB Inactive: 56808 kB HighTotal: 131008 kB HighFree: 46116 kB LowTotal: 903652 kB LowFree: 843588 kB SwapTotal: 2097892 kB SwapFree: 2096456 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5708 kB Slab: 19192 kB Committed_AS: 64368 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:06:03 (client local time) WITH STATUS 0 IN 1207.33 SECONDS stats: 2967 7 1207.33 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/4648/stat): 4648 (minisat+_script) R 4647 4648 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1729072121 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/4648/statm): 174 3 169 147 0 27 0 [pid=4648] 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=4649 New process pid=4650 New process pid=4651 execve syscall for /bin/sed executable One traced child (pid=4650) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=4651) exited with status: 0 One traced child (pid=4649) exited with status: 0 New process pid=4652 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-dcmulti.opb [startup+10.0038 s] Raw data (loadavg): 0.93 0.95 0.71 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11550 0 4 0 888 50 0 0 25 0 1 0 1729072126 56516608 11160 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 13798 11160 145 145 0 13653 0 [pid=4652] vsize: 55192 Current children cumulated CPU time (s) 9.4 Current children cumulated vsize (Kb) 57316 [startup+20.0045 s] Raw data (loadavg): 0.94 0.96 0.71 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11590 0 4 0 1888 50 0 0 25 0 1 0 1729072126 56668160 11200 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 13835 11200 145 145 0 13690 0 [pid=4652] vsize: 55340 Current children cumulated CPU time (s) 19.4 Current children cumulated vsize (Kb) 57464 [startup+30.0051 s] Raw data (loadavg): 0.95 0.96 0.71 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11611 0 4 0 2887 50 0 0 25 0 1 0 1729072126 56741888 11221 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 13853 11221 145 145 0 13708 0 [pid=4652] vsize: 55412 Current children cumulated CPU time (s) 29.39 Current children cumulated vsize (Kb) 57536 [startup+40.0058 s] Raw data (loadavg): 0.96 0.96 0.71 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11645 0 4 0 3887 51 0 0 25 0 1 0 1729072126 56823808 11255 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 13873 11255 145 145 0 13728 0 [pid=4652] vsize: 55492 Current children cumulated CPU time (s) 39.4 Current children cumulated vsize (Kb) 57616 [startup+50.0065 s] Raw data (loadavg): 0.96 0.96 0.72 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11686 0 4 0 4886 52 0 0 25 0 1 0 1729072126 56975360 11296 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 13910 11296 145 145 0 13765 0 [pid=4652] vsize: 55640 Current children cumulated CPU time (s) 49.4 Current children cumulated vsize (Kb) 57764 [startup+60.0072 s] Raw data (loadavg): 0.97 0.96 0.72 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11713 0 4 0 5885 52 0 0 25 0 1 0 1729072126 57061376 11323 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 13931 11323 145 145 0 13786 0 [pid=4652] vsize: 55724 Current children cumulated CPU time (s) 59.39 Current children cumulated vsize (Kb) 57848 [startup+70.0079 s] Raw data (loadavg): 0.97 0.96 0.72 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11732 0 4 0 6885 52 0 0 25 0 1 0 1729072126 57135104 11342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 13949 11342 145 145 0 13804 0 [pid=4652] vsize: 55796 Current children cumulated CPU time (s) 69.39 Current children cumulated vsize (Kb) 57920 [startup+80.0086 s] Raw data (loadavg): 0.98 0.96 0.73 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11766 0 4 0 7885 53 0 0 25 0 1 0 1729072126 57266176 11376 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 13981 11376 145 145 0 13836 0 [pid=4652] vsize: 55924 Current children cumulated CPU time (s) 79.4 Current children cumulated vsize (Kb) 58048 [startup+90.0093 s] Raw data (loadavg): 0.98 0.96 0.73 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11785 0 4 0 8885 53 0 0 25 0 1 0 1729072126 57335808 11395 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 13998 11395 145 145 0 13853 0 [pid=4652] vsize: 55992 Current children cumulated CPU time (s) 89.4 Current children cumulated vsize (Kb) 58116 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.73 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 11890 0 4 0 9883 54 0 0 25 0 1 0 1729072126 57749504 11500 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 14099 11500 145 145 0 13954 0 [pid=4652] vsize: 56396 Current children cumulated CPU time (s) 99.39 Current children cumulated vsize (Kb) 58520 [startup+110.01 s] Raw data (loadavg): 0.98 0.96 0.73 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 12173 0 4 0 10879 55 0 0 25 0 1 0 1729072126 58945536 11783 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 14391 11783 145 145 0 14246 0 [pid=4652] vsize: 57564 Current children cumulated CPU time (s) 109.36 Current children cumulated vsize (Kb) 59688 [startup+120.01 s] Raw data (loadavg): 0.99 0.97 0.73 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 12417 0 4 0 11874 57 0 0 25 0 1 0 1729072126 59924480 12027 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 14630 12027 145 145 0 14485 0 [pid=4652] vsize: 58520 Current children cumulated CPU time (s) 119.33 Current children cumulated vsize (Kb) 60644 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.74 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 12746 0 4 0 12869 60 0 0 25 0 1 0 1729072126 61374464 12356 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 14984 12356 145 145 0 14839 0 [pid=4652] vsize: 59936 Current children cumulated CPU time (s) 129.31 Current children cumulated vsize (Kb) 62060 [startup+140.011 s] Raw data (loadavg): 0.99 0.97 0.74 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13029 0 4 0 13865 61 0 0 25 0 1 0 1729072126 62504960 12639 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 15260 12639 145 145 0 15115 0 [pid=4652] vsize: 61040 Current children cumulated CPU time (s) 139.28 Current children cumulated vsize (Kb) 63164 [startup+150.011 s] Raw data (loadavg): 0.99 0.97 0.74 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13298 0 4 0 14860 63 0 0 25 0 1 0 1729072126 63582208 12908 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 15523 12908 145 145 0 15378 0 [pid=4652] vsize: 62092 Current children cumulated CPU time (s) 149.25 Current children cumulated vsize (Kb) 64216 [startup+160.011 s] Raw data (loadavg): 0.99 0.97 0.74 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13454 0 4 0 15857 66 0 0 25 0 1 0 1729072126 64204800 13064 4294967295 134512640 135094434 3221224432 3221223024 134551780 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 15675 13064 145 145 0 15530 0 [pid=4652] vsize: 62700 Current children cumulated CPU time (s) 159.25 Current children cumulated vsize (Kb) 64824 [startup+170.012 s] Raw data (loadavg): 0.99 0.97 0.74 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 13748 0 4 0 16851 69 0 0 25 0 1 0 1729072126 65384448 13358 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 15963 13358 145 145 0 15818 0 [pid=4652] vsize: 63852 Current children cumulated CPU time (s) 169.22 Current children cumulated vsize (Kb) 65976 [startup+180.012 s] Raw data (loadavg): 0.99 0.97 0.75 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 14124 0 4 0 17845 72 0 0 25 0 1 0 1729072126 66899968 13734 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 16333 13734 145 145 0 16188 0 [pid=4652] vsize: 65332 Current children cumulated CPU time (s) 179.19 Current children cumulated vsize (Kb) 67456 [startup+190.012 s] Raw data (loadavg): 0.99 0.97 0.75 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 14504 0 4 0 18838 75 0 0 25 0 1 0 1729072126 68681728 14114 4294967295 134512640 135094434 3221224432 3221223104 134555310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 16768 14114 145 145 0 16623 0 [pid=4652] vsize: 67072 Current children cumulated CPU time (s) 189.15 Current children cumulated vsize (Kb) 69196 [startup+200.013 s] Raw data (loadavg): 0.99 0.97 0.75 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 14924 0 4 0 19831 78 0 0 25 0 1 0 1729072126 70377472 14534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 17182 14534 145 145 0 17037 0 [pid=4652] vsize: 68728 Current children cumulated CPU time (s) 199.11 Current children cumulated vsize (Kb) 70852 [startup+210.014 s] Raw data (loadavg): 0.99 0.97 0.75 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 15452 0 4 0 20822 82 0 0 25 0 1 0 1729072126 72503296 15062 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 17701 15062 145 145 0 17556 0 [pid=4652] vsize: 70804 Current children cumulated CPU time (s) 209.06 Current children cumulated vsize (Kb) 72928 [startup+220.014 s] Raw data (loadavg): 0.99 0.97 0.75 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 15889 0 4 0 21815 84 0 0 25 0 1 0 1729072126 74264576 15499 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 18131 15499 145 145 0 17986 0 [pid=4652] vsize: 72524 Current children cumulated CPU time (s) 219.01 Current children cumulated vsize (Kb) 74648 [startup+230.015 s] Raw data (loadavg): 0.99 0.97 0.76 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16100 0 4 0 22813 85 0 0 25 0 1 0 1729072126 75108352 15710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 18337 15710 145 145 0 18192 0 [pid=4652] vsize: 73348 Current children cumulated CPU time (s) 229 Current children cumulated vsize (Kb) 75472 [startup+240.016 s] Raw data (loadavg): 0.99 0.97 0.76 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16360 0 4 0 23809 87 0 0 25 0 1 0 1729072126 76148736 15970 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 18591 15970 145 145 0 18446 0 [pid=4652] vsize: 74364 Current children cumulated CPU time (s) 238.98 Current children cumulated vsize (Kb) 76488 [startup+250.016 s] Raw data (loadavg): 0.99 0.97 0.76 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16619 0 4 0 24805 89 0 0 25 0 1 0 1729072126 77189120 16229 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 18845 16229 145 145 0 18700 0 [pid=4652] vsize: 75380 Current children cumulated CPU time (s) 248.96 Current children cumulated vsize (Kb) 77504 [startup+260.016 s] Raw data (loadavg): 0.99 0.97 0.76 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 16818 0 4 0 25801 90 0 0 25 0 1 0 1729072126 77983744 16428 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 19039 16428 145 145 0 18894 0 [pid=4652] vsize: 76156 Current children cumulated CPU time (s) 258.93 Current children cumulated vsize (Kb) 78280 [startup+270.017 s] Raw data (loadavg): 0.99 0.97 0.76 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17201 0 4 0 26795 93 0 0 25 0 1 0 1729072126 79523840 16811 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 19415 16811 145 145 0 19270 0 [pid=4652] vsize: 77660 Current children cumulated CPU time (s) 268.9 Current children cumulated vsize (Kb) 79784 [startup+280.018 s] Raw data (loadavg): 0.99 0.97 0.77 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17491 0 4 0 27789 95 0 0 25 0 1 0 1729072126 81231872 17101 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 19832 17101 145 145 0 19687 0 [pid=4652] vsize: 79328 Current children cumulated CPU time (s) 278.86 Current children cumulated vsize (Kb) 81452 [startup+290.019 s] Raw data (loadavg): 0.99 0.97 0.77 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17714 0 4 0 28785 96 0 0 25 0 1 0 1729072126 82128896 17324 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 20051 17324 145 145 0 19906 0 [pid=4652] vsize: 80204 Current children cumulated CPU time (s) 288.83 Current children cumulated vsize (Kb) 82328 [startup+300.019 s] Raw data (loadavg): 0.99 0.97 0.77 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 17866 0 4 0 29781 98 0 0 25 0 1 0 1729072126 82739200 17476 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 20200 17476 145 145 0 20055 0 [pid=4652] vsize: 80800 Current children cumulated CPU time (s) 298.81 Current children cumulated vsize (Kb) 82924 [startup+310.02 s] Raw data (loadavg): 0.99 0.97 0.77 1/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 17979 0 4 0 30779 99 0 0 25 0 1 0 1729072126 83189760 17589 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/4652/statm): 20310 17589 145 145 0 20165 0 [pid=4652] vsize: 81240 Current children cumulated CPU time (s) 308.8 Current children cumulated vsize (Kb) 83364 [startup+320.021 s] Raw data (loadavg): 0.99 0.97 0.77 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 18279 0 4 0 31774 101 0 0 25 0 1 0 1729072126 84402176 17889 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 20606 17889 145 145 0 20461 0 [pid=4652] vsize: 82424 Current children cumulated CPU time (s) 318.77 Current children cumulated vsize (Kb) 84548 [startup+330.021 s] Raw data (loadavg): 0.99 0.97 0.78 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 18567 0 4 0 32770 103 0 0 25 0 1 0 1729072126 85565440 18177 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 20890 18177 145 145 0 20745 0 [pid=4652] vsize: 83560 Current children cumulated CPU time (s) 328.75 Current children cumulated vsize (Kb) 85684 [startup+340.022 s] Raw data (loadavg): 0.99 0.97 0.78 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 18808 0 4 0 33766 105 0 0 25 0 1 0 1729072126 86528000 18418 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 21125 18418 145 145 0 20980 0 [pid=4652] vsize: 84500 Current children cumulated CPU time (s) 338.73 Current children cumulated vsize (Kb) 86624 [startup+350.022 s] Raw data (loadavg): 0.99 0.97 0.78 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19037 0 4 0 34763 106 0 0 25 0 1 0 1729072126 87449600 18647 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 21350 18647 145 145 0 21205 0 [pid=4652] vsize: 85400 Current children cumulated CPU time (s) 348.71 Current children cumulated vsize (Kb) 87524 [startup+360.023 s] Raw data (loadavg): 0.99 0.97 0.78 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19315 0 4 0 35759 108 0 0 25 0 1 0 1729072126 88563712 18925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 21622 18925 145 145 0 21477 0 [pid=4652] vsize: 86488 Current children cumulated CPU time (s) 358.69 Current children cumulated vsize (Kb) 88612 [startup+370.023 s] Raw data (loadavg): 0.99 0.97 0.78 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19598 0 4 0 36753 110 0 0 25 0 1 0 1729072126 89702400 19208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 21900 19208 145 145 0 21755 0 [pid=4652] vsize: 87600 Current children cumulated CPU time (s) 368.65 Current children cumulated vsize (Kb) 89724 [startup+380.023 s] Raw data (loadavg): 0.99 0.97 0.79 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 19917 0 4 0 37748 112 0 0 25 0 1 0 1729072126 90996736 19527 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 22216 19527 145 145 0 22071 0 [pid=4652] vsize: 88864 Current children cumulated CPU time (s) 378.62 Current children cumulated vsize (Kb) 90988 [startup+390.024 s] Raw data (loadavg): 0.99 0.97 0.79 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20206 0 4 0 38743 114 0 0 25 0 1 0 1729072126 92168192 19816 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 22502 19816 145 145 0 22357 0 [pid=4652] vsize: 90008 Current children cumulated CPU time (s) 388.59 Current children cumulated vsize (Kb) 92132 [startup+400.024 s] Raw data (loadavg): 0.99 0.97 0.79 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20470 0 4 0 39739 115 0 0 25 0 1 0 1729072126 93253632 20080 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 22767 20080 145 145 0 22622 0 [pid=4652] vsize: 91068 Current children cumulated CPU time (s) 398.56 Current children cumulated vsize (Kb) 93192 [startup+410.025 s] Raw data (loadavg): 0.99 0.97 0.79 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20740 0 4 0 40734 117 0 0 25 0 1 0 1729072126 94367744 20350 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 23039 20350 145 145 0 22894 0 [pid=4652] vsize: 92156 Current children cumulated CPU time (s) 408.53 Current children cumulated vsize (Kb) 94280 [startup+420.026 s] Raw data (loadavg): 0.99 0.97 0.79 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20840 0 4 0 41732 118 0 0 25 0 1 0 1729072126 94785536 20450 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 23141 20450 145 145 0 22996 0 [pid=4652] vsize: 92564 Current children cumulated CPU time (s) 418.52 Current children cumulated vsize (Kb) 94688 [startup+430.027 s] Raw data (loadavg): 0.99 0.97 0.80 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 20896 0 4 0 42732 118 0 0 25 0 1 0 1729072126 95031296 20506 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4652/statm): 23201 20506 145 145 0 23056 0 [pid=4652] vsize: 92804 Current children cumulated CPU time (s) 428.52 Current children cumulated vsize (Kb) 94928 [startup+440.027 s] Raw data (loadavg): 0.99 0.97 0.80 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21126 0 4 0 43727 121 0 0 25 0 1 0 1729072126 95989760 20736 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 23435 20736 145 145 0 23290 0 [pid=4652] vsize: 93740 Current children cumulated CPU time (s) 438.5 Current children cumulated vsize (Kb) 95864 [startup+450.028 s] Raw data (loadavg): 0.99 0.97 0.80 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21335 0 4 0 44724 122 0 0 25 0 1 0 1729072126 96845824 20945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 23644 20945 145 145 0 23499 0 [pid=4652] vsize: 94576 Current children cumulated CPU time (s) 448.48 Current children cumulated vsize (Kb) 96700 [startup+460.029 s] Raw data (loadavg): 0.99 0.97 0.80 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21567 0 4 0 45721 123 0 0 25 0 1 0 1729072126 97771520 21177 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 23870 21177 145 145 0 23725 0 [pid=4652] vsize: 95480 Current children cumulated CPU time (s) 458.46 Current children cumulated vsize (Kb) 97604 [startup+470.029 s] Raw data (loadavg): 0.99 0.97 0.80 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21779 0 4 0 46717 124 0 0 25 0 1 0 1729072126 98631680 21389 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 24080 21389 145 145 0 23935 0 [pid=4652] vsize: 96320 Current children cumulated CPU time (s) 468.43 Current children cumulated vsize (Kb) 98444 [startup+480.029 s] Raw data (loadavg): 0.99 0.97 0.81 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 21957 0 4 0 47715 125 0 0 25 0 1 0 1729072126 99344384 21567 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 24254 21567 145 145 0 24109 0 [pid=4652] vsize: 97016 Current children cumulated CPU time (s) 478.42 Current children cumulated vsize (Kb) 99140 [startup+490.03 s] Raw data (loadavg): 0.99 0.97 0.81 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22180 0 4 0 48712 126 0 0 25 0 1 0 1729072126 100274176 21790 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 24481 21790 145 145 0 24336 0 [pid=4652] vsize: 97924 Current children cumulated CPU time (s) 488.4 Current children cumulated vsize (Kb) 100048 [startup+500.031 s] Raw data (loadavg): 0.99 0.97 0.81 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22356 0 4 0 49709 128 0 0 25 0 1 0 1729072126 100990976 21966 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 24656 21966 145 145 0 24511 0 [pid=4652] vsize: 98624 Current children cumulated CPU time (s) 498.39 Current children cumulated vsize (Kb) 100748 [startup+510.031 s] Raw data (loadavg): 0.99 0.97 0.81 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22525 0 4 0 50706 129 0 0 25 0 1 0 1729072126 101670912 22135 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 24822 22135 145 145 0 24677 0 [pid=4652] vsize: 99288 Current children cumulated CPU time (s) 508.37 Current children cumulated vsize (Kb) 101412 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.81 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 22815 0 4 0 51700 131 0 0 25 0 1 0 1729072126 102834176 22425 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 25106 22425 145 145 0 24961 0 [pid=4652] vsize: 100424 Current children cumulated CPU time (s) 518.33 Current children cumulated vsize (Kb) 102548 [startup+530.032 s] Raw data (loadavg): 0.99 0.97 0.81 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 23032 0 4 0 52696 133 0 0 25 0 1 0 1729072126 103706624 22642 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 25319 22642 145 145 0 25174 0 [pid=4652] vsize: 101276 Current children cumulated CPU time (s) 528.31 Current children cumulated vsize (Kb) 103400 [startup+540.032 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 23326 0 4 0 53690 136 0 0 25 0 1 0 1729072126 104910848 22936 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 25613 22936 145 145 0 25468 0 [pid=4652] vsize: 102452 Current children cumulated CPU time (s) 538.28 Current children cumulated vsize (Kb) 104576 [startup+550.032 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 23470 0 4 0 54688 137 0 0 25 0 1 0 1729072126 105492480 23080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 25755 23080 145 145 0 25610 0 [pid=4652] vsize: 103020 Current children cumulated CPU time (s) 548.27 Current children cumulated vsize (Kb) 105144 [startup+560.033 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 23754 0 4 0 55682 138 0 0 25 0 1 0 1729072126 106631168 23364 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/4652/statm): 26033 23364 145 145 0 25888 0 [pid=4652] vsize: 104132 Current children cumulated CPU time (s) 558.22 Current children cumulated vsize (Kb) 106256 [startup+570.033 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24019 0 4 0 56678 141 0 0 25 0 1 0 1729072126 107704320 23629 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 26295 23629 145 145 0 26150 0 [pid=4652] vsize: 105180 Current children cumulated CPU time (s) 568.21 Current children cumulated vsize (Kb) 107304 [startup+580.034 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24398 0 4 0 57671 144 0 0 25 0 1 0 1729072126 109252608 24008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 26673 24008 145 145 0 26528 0 [pid=4652] vsize: 106692 Current children cumulated CPU time (s) 578.17 Current children cumulated vsize (Kb) 108816 [startup+590.035 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24538 0 4 0 58668 145 0 0 25 0 1 0 1729072126 109821952 24148 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 26812 24148 145 145 0 26667 0 [pid=4652] vsize: 107248 Current children cumulated CPU time (s) 588.15 Current children cumulated vsize (Kb) 109372 [startup+600.035 s] Raw data (loadavg): 0.99 0.97 0.82 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24699 0 4 0 59666 146 0 0 25 0 1 0 1729072126 111525888 24309 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 27228 24309 145 145 0 27083 0 [pid=4652] vsize: 108912 Current children cumulated CPU time (s) 598.14 Current children cumulated vsize (Kb) 111036 [startup+610.036 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24839 0 4 0 60663 147 0 0 25 0 1 0 1729072126 112115712 24449 4294967295 134512640 135094434 3221224432 3221222912 134780630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 27372 24449 145 145 0 27227 0 [pid=4652] vsize: 109488 Current children cumulated CPU time (s) 608.12 Current children cumulated vsize (Kb) 111612 [startup+620.037 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 24930 0 4 0 61663 147 0 0 25 0 1 0 1729072126 112480256 24540 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 27461 24540 145 145 0 27316 0 [pid=4652] vsize: 109844 Current children cumulated CPU time (s) 618.12 Current children cumulated vsize (Kb) 111968 [startup+630.037 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25064 0 4 0 62661 148 0 0 25 0 1 0 1729072126 113020928 24674 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 27593 24674 145 145 0 27448 0 [pid=4652] vsize: 110372 Current children cumulated CPU time (s) 628.11 Current children cumulated vsize (Kb) 112496 [startup+640.038 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25195 0 4 0 63659 149 0 0 25 0 1 0 1729072126 113549312 24805 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 27722 24805 145 145 0 27577 0 [pid=4652] vsize: 110888 Current children cumulated CPU time (s) 638.1 Current children cumulated vsize (Kb) 113012 [startup+650.039 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25410 0 4 0 64654 151 0 0 25 0 1 0 1729072126 114413568 25020 4294967295 134512640 135094434 3221224432 3221223056 134557630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 27933 25020 145 145 0 27788 0 [pid=4652] vsize: 111732 Current children cumulated CPU time (s) 648.07 Current children cumulated vsize (Kb) 113856 [startup+660.04 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25681 0 4 0 65650 153 0 0 25 0 1 0 1729072126 115494912 25291 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 28197 25291 145 145 0 28052 0 [pid=4652] vsize: 112788 Current children cumulated CPU time (s) 658.05 Current children cumulated vsize (Kb) 114912 [startup+670.04 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 25858 0 4 0 66647 155 0 0 25 0 1 0 1729072126 116228096 25468 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 28376 25468 145 145 0 28231 0 [pid=4652] vsize: 113504 Current children cumulated CPU time (s) 668.04 Current children cumulated vsize (Kb) 115628 [startup+680.041 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26057 0 4 0 67643 156 0 0 25 0 1 0 1729072126 117018624 25667 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 28569 25667 145 145 0 28424 0 [pid=4652] vsize: 114276 Current children cumulated CPU time (s) 678.01 Current children cumulated vsize (Kb) 116400 [startup+690.042 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26223 0 4 0 68640 158 0 0 25 0 1 0 1729072126 117690368 25833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 28733 25833 145 145 0 28588 0 [pid=4652] vsize: 114932 Current children cumulated CPU time (s) 688 Current children cumulated vsize (Kb) 117056 [startup+700.043 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26392 0 4 0 69637 160 0 0 25 0 1 0 1729072126 118378496 26002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 28901 26002 145 145 0 28756 0 [pid=4652] vsize: 115604 Current children cumulated CPU time (s) 697.99 Current children cumulated vsize (Kb) 117728 [startup+710.043 s] Raw data (loadavg): 0.99 0.97 0.83 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26515 0 4 0 70634 160 0 0 25 0 1 0 1729072126 118874112 26125 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29022 26125 145 145 0 28877 0 [pid=4652] vsize: 116088 Current children cumulated CPU time (s) 707.96 Current children cumulated vsize (Kb) 118212 [startup+720.044 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26674 0 4 0 71631 161 0 0 25 0 1 0 1729072126 119508992 26284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29177 26284 145 145 0 29032 0 [pid=4652] vsize: 116708 Current children cumulated CPU time (s) 717.94 Current children cumulated vsize (Kb) 118832 [startup+730.044 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 26869 0 4 0 72628 163 0 0 25 0 1 0 1729072126 120295424 26479 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29369 26479 145 145 0 29224 0 [pid=4652] vsize: 117476 Current children cumulated CPU time (s) 727.93 Current children cumulated vsize (Kb) 119600 [startup+740.044 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 27063 0 4 0 73625 164 0 0 25 0 1 0 1729072126 121065472 26673 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29557 26673 145 145 0 29412 0 [pid=4652] vsize: 118228 Current children cumulated CPU time (s) 737.91 Current children cumulated vsize (Kb) 120352 [startup+750.045 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27210 0 4 0 74623 165 0 0 25 0 1 0 1729072126 121659392 26820 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29702 26820 145 145 0 29557 0 [pid=4652] vsize: 118808 Current children cumulated CPU time (s) 747.9 Current children cumulated vsize (Kb) 120932 [startup+760.046 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27352 0 4 0 75620 167 0 0 25 0 1 0 1729072126 122273792 26962 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29852 26962 145 145 0 29707 0 [pid=4652] vsize: 119408 Current children cumulated CPU time (s) 757.89 Current children cumulated vsize (Kb) 121532 [startup+770.046 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27485 0 4 0 76617 168 0 0 25 0 1 0 1729072126 122798080 27095 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 29980 27095 145 145 0 29835 0 [pid=4652] vsize: 119920 Current children cumulated CPU time (s) 767.87 Current children cumulated vsize (Kb) 122044 [startup+780.047 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27615 0 4 0 77615 169 0 0 25 0 1 0 1729072126 123322368 27225 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30108 27225 145 145 0 29963 0 [pid=4652] vsize: 120432 Current children cumulated CPU time (s) 777.86 Current children cumulated vsize (Kb) 122556 [startup+790.048 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27732 0 4 0 78613 171 0 0 25 0 1 0 1729072126 123809792 27342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30227 27342 145 145 0 30082 0 [pid=4652] vsize: 120908 Current children cumulated CPU time (s) 787.86 Current children cumulated vsize (Kb) 123032 [startup+800.048 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 27908 0 4 0 79610 172 0 0 25 0 1 0 1729072126 124534784 27518 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30404 27518 145 145 0 30259 0 [pid=4652] vsize: 121616 Current children cumulated CPU time (s) 797.84 Current children cumulated vsize (Kb) 123740 [startup+810.05 s] Raw data (loadavg): 0.99 0.97 0.84 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28056 0 4 0 80609 173 0 0 25 0 1 0 1729072126 125132800 27666 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30550 27666 145 145 0 30405 0 [pid=4652] vsize: 122200 Current children cumulated CPU time (s) 807.84 Current children cumulated vsize (Kb) 124324 [startup+820.052 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28216 0 4 0 81606 174 0 0 25 0 1 0 1729072126 125775872 27826 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30707 27826 145 145 0 30562 0 [pid=4652] vsize: 122828 Current children cumulated CPU time (s) 817.82 Current children cumulated vsize (Kb) 124952 [startup+830.052 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28332 0 4 0 82605 174 0 0 25 0 1 0 1729072126 126259200 27942 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30825 27942 145 145 0 30680 0 [pid=4652] vsize: 123300 Current children cumulated CPU time (s) 827.81 Current children cumulated vsize (Kb) 125424 [startup+840.052 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28464 0 4 0 83603 176 0 0 25 0 1 0 1729072126 126791680 28074 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 30955 28074 145 145 0 30810 0 [pid=4652] vsize: 123820 Current children cumulated CPU time (s) 837.81 Current children cumulated vsize (Kb) 125944 [startup+850.053 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28660 0 4 0 84599 177 0 0 25 0 1 0 1729072126 127586304 28270 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 31149 28270 145 145 0 31004 0 [pid=4652] vsize: 124596 Current children cumulated CPU time (s) 847.78 Current children cumulated vsize (Kb) 126720 [startup+860.054 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28839 0 4 0 85597 178 0 0 25 0 1 0 1729072126 128307200 28449 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 31325 28449 145 145 0 31180 0 [pid=4652] vsize: 125300 Current children cumulated CPU time (s) 857.77 Current children cumulated vsize (Kb) 127424 [startup+870.054 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 28989 0 4 0 86594 179 0 0 25 0 1 0 1729072126 128925696 28599 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 31476 28599 145 145 0 31331 0 [pid=4652] vsize: 125904 Current children cumulated CPU time (s) 867.75 Current children cumulated vsize (Kb) 128028 [startup+880.055 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29118 0 4 0 87592 180 0 0 25 0 1 0 1729072126 129454080 28728 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 31605 28728 145 145 0 31460 0 [pid=4652] vsize: 126420 Current children cumulated CPU time (s) 877.74 Current children cumulated vsize (Kb) 128544 [startup+890.056 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29327 0 4 0 88588 181 0 0 25 0 1 0 1729072126 130293760 28937 4294967295 134512640 135094434 3221224432 3221223092 134553466 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 31810 28937 145 145 0 31665 0 [pid=4652] vsize: 127240 Current children cumulated CPU time (s) 887.71 Current children cumulated vsize (Kb) 129364 [startup+900.056 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4652 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29477 0 4 0 89585 182 0 0 25 0 1 0 1729072126 130891776 29087 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 31956 29087 145 145 0 31811 0 [pid=4652] vsize: 127824 Current children cumulated CPU time (s) 897.69 Current children cumulated vsize (Kb) 129948 [startup+910.057 s] Raw data (loadavg): 0.99 0.97 0.85 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29562 0 4 0 90585 183 0 0 25 0 1 0 1729072126 131244032 29172 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32042 29172 145 145 0 31897 0 [pid=4652] vsize: 128168 Current children cumulated CPU time (s) 907.7 Current children cumulated vsize (Kb) 130292 [startup+920.058 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29681 0 4 0 91583 183 0 0 25 0 1 0 1729072126 131723264 29291 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32159 29291 145 145 0 32014 0 [pid=4652] vsize: 128636 Current children cumulated CPU time (s) 917.68 Current children cumulated vsize (Kb) 130760 [startup+930.058 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29811 0 4 0 92580 184 0 0 25 0 1 0 1729072126 132251648 29421 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32288 29421 145 145 0 32143 0 [pid=4652] vsize: 129152 Current children cumulated CPU time (s) 927.66 Current children cumulated vsize (Kb) 131276 [startup+940.058 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 29934 0 4 0 93578 186 0 0 25 0 1 0 1729072126 132743168 29544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32408 29544 145 145 0 32263 0 [pid=4652] vsize: 129632 Current children cumulated CPU time (s) 937.66 Current children cumulated vsize (Kb) 131756 [startup+950.059 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30070 0 4 0 94575 186 0 0 25 0 1 0 1729072126 133279744 29680 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32539 29680 145 145 0 32394 0 [pid=4652] vsize: 130156 Current children cumulated CPU time (s) 947.63 Current children cumulated vsize (Kb) 132280 [startup+960.06 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30211 0 4 0 95573 188 0 0 25 0 1 0 1729072126 133861376 29821 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32681 29821 145 145 0 32536 0 [pid=4652] vsize: 130724 Current children cumulated CPU time (s) 957.63 Current children cumulated vsize (Kb) 132848 [startup+970.06 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30366 0 4 0 96570 189 0 0 25 0 1 0 1729072126 134475776 29976 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32831 29976 145 145 0 32686 0 [pid=4652] vsize: 131324 Current children cumulated CPU time (s) 967.61 Current children cumulated vsize (Kb) 133448 [startup+980.06 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30512 0 4 0 97567 190 0 0 25 0 1 0 1729072126 135065600 30122 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 32975 30122 145 145 0 32830 0 [pid=4652] vsize: 131900 Current children cumulated CPU time (s) 977.59 Current children cumulated vsize (Kb) 134024 [startup+990.061 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30666 0 4 0 98564 192 0 0 25 0 1 0 1729072126 135720960 30276 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 33135 30276 145 145 0 32990 0 [pid=4652] vsize: 132540 Current children cumulated CPU time (s) 987.58 Current children cumulated vsize (Kb) 134664 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30821 0 4 0 99561 193 0 0 25 0 1 0 1729072126 136372224 30431 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 33294 30431 145 145 0 33149 0 [pid=4652] vsize: 133176 Current children cumulated CPU time (s) 997.56 Current children cumulated vsize (Kb) 135300 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.86 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 30952 0 4 0 100559 194 0 0 25 0 1 0 1729072126 136900608 30562 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 33423 30562 145 145 0 33278 0 [pid=4652] vsize: 133692 Current children cumulated CPU time (s) 1007.55 Current children cumulated vsize (Kb) 135816 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31083 0 4 0 101557 195 0 0 25 0 1 0 1729072126 137433088 30693 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 33553 30693 145 145 0 33408 0 [pid=4652] vsize: 134212 Current children cumulated CPU time (s) 1017.54 Current children cumulated vsize (Kb) 136336 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31314 0 4 0 102553 197 0 0 25 0 1 0 1729072126 138362880 30924 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 33780 30924 145 145 0 33635 0 [pid=4652] vsize: 135120 Current children cumulated CPU time (s) 1027.52 Current children cumulated vsize (Kb) 137244 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31545 0 4 0 103548 199 0 0 25 0 1 0 1729072126 139292672 31155 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 34007 31155 145 145 0 33862 0 [pid=4652] vsize: 136028 Current children cumulated CPU time (s) 1037.49 Current children cumulated vsize (Kb) 138152 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 31768 0 4 0 104544 200 0 0 25 0 1 0 1729072126 140283904 31378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 34249 31378 145 145 0 34104 0 [pid=4652] vsize: 136996 Current children cumulated CPU time (s) 1047.46 Current children cumulated vsize (Kb) 139120 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32037 0 4 0 105539 202 0 0 25 0 1 0 1729072126 141369344 31647 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 34514 31647 145 145 0 34369 0 [pid=4652] vsize: 138056 Current children cumulated CPU time (s) 1057.43 Current children cumulated vsize (Kb) 140180 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32323 0 4 0 106535 203 0 0 25 0 1 0 1729072126 142528512 31933 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 34797 31933 145 145 0 34652 0 [pid=4652] vsize: 139188 Current children cumulated CPU time (s) 1067.4 Current children cumulated vsize (Kb) 141312 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32574 0 4 0 107531 204 0 0 25 0 1 0 1729072126 143552512 32184 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35047 32184 145 145 0 34902 0 [pid=4652] vsize: 140188 Current children cumulated CPU time (s) 1077.37 Current children cumulated vsize (Kb) 142312 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 32708 0 4 0 108529 206 0 0 25 0 1 0 1729072126 144084992 32318 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35177 32318 145 145 0 35032 0 [pid=4652] vsize: 140708 Current children cumulated CPU time (s) 1087.37 Current children cumulated vsize (Kb) 142832 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.87 1/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) T 4648 4648 20602 0 -1 0 32850 0 4 0 109527 207 0 0 25 0 1 0 1729072126 144666624 32460 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35319 32460 145 145 0 35174 0 [pid=4652] vsize: 141276 Current children cumulated CPU time (s) 1097.36 Current children cumulated vsize (Kb) 143400 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33107 0 4 0 110522 209 0 0 25 0 1 0 1729072126 145694720 32717 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35570 32717 145 145 0 35425 0 [pid=4652] vsize: 142280 Current children cumulated CPU time (s) 1107.33 Current children cumulated vsize (Kb) 144404 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.87 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33252 0 4 0 111521 210 0 0 25 0 1 0 1729072126 146264064 32862 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35709 32862 145 145 0 35564 0 [pid=4652] vsize: 142836 Current children cumulated CPU time (s) 1117.33 Current children cumulated vsize (Kb) 144960 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33389 0 4 0 112518 211 0 0 25 0 1 0 1729072126 146817024 32999 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35844 32999 145 145 0 35699 0 [pid=4652] vsize: 143376 Current children cumulated CPU time (s) 1127.31 Current children cumulated vsize (Kb) 145500 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33448 0 4 0 113518 211 0 0 25 0 1 0 1729072126 147091456 33058 4294967295 134512640 135094434 3221224432 3221223044 134563092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 35911 33058 145 145 0 35766 0 [pid=4652] vsize: 143644 Current children cumulated CPU time (s) 1137.31 Current children cumulated vsize (Kb) 145768 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33539 0 4 0 114517 212 0 0 25 0 1 0 1729072126 147501056 33149 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36011 33149 145 145 0 35866 0 [pid=4652] vsize: 144044 Current children cumulated CPU time (s) 1147.31 Current children cumulated vsize (Kb) 146168 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33617 0 4 0 115516 213 0 0 25 0 1 0 1729072126 147857408 33227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36098 33227 145 145 0 35953 0 [pid=4652] vsize: 144392 Current children cumulated CPU time (s) 1157.31 Current children cumulated vsize (Kb) 146516 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33708 0 4 0 116515 214 0 0 25 0 1 0 1729072126 148262912 33318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36197 33318 145 145 0 36052 0 [pid=4652] vsize: 144788 Current children cumulated CPU time (s) 1167.31 Current children cumulated vsize (Kb) 146912 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33807 0 4 0 117514 214 0 0 25 0 1 0 1729072126 148652032 33417 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36292 33417 145 145 0 36147 0 [pid=4652] vsize: 145168 Current children cumulated CPU time (s) 1177.3 Current children cumulated vsize (Kb) 147292 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33902 0 4 0 118512 215 0 0 25 0 1 0 1729072126 149057536 33512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36391 33512 145 145 0 36246 0 [pid=4652] vsize: 145564 Current children cumulated CPU time (s) 1187.29 Current children cumulated vsize (Kb) 147688 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 33999 0 4 0 119510 216 0 0 25 0 1 0 1729072126 149438464 33609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36484 33609 145 145 0 36339 0 [pid=4652] vsize: 145936 Current children cumulated CPU time (s) 1197.28 Current children cumulated vsize (Kb) 148060 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 34091 0 4 0 120509 216 0 0 25 0 1 0 1729072126 149807104 33701 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36574 33701 145 145 0 36429 0 [pid=4652] vsize: 146296 Current children cumulated CPU time (s) 1207.27 Current children cumulated vsize (Kb) 148420 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.88 2/58 4654 Raw data (/proc/4648/stat): 4648 (minisat+_script) S 4647 4648 20602 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1729072121 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4648/statm): 531 226 485 147 0 384 0 [pid=4648] vsize: 2124 Raw data (/proc/4652/stat): 4652 (minisat+_64-bit) R 4648 4648 20602 0 -1 0 34091 0 4 0 120509 216 0 0 25 0 1 0 1729072126 149807104 33701 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4652/statm): 36574 33701 145 145 0 36429 0 [pid=4652] vsize: 146296 Current children cumulated CPU time (s) 1207.27 Current children cumulated vsize (Kb) 148420 Sending SIGTERM to -4648 Sleeping 2 seconds One traced child (pid=4648) ended because it received signal 15 (SIGTERM) One traced child (pid=4652) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1207.33 CPU user time (s): 1205.1 CPU system time (s): 2.23066 CPU usage (%): 99.7678 Max. virtual memory (cumulated for all children) (Kb): 148420
ERROR: no interpretation found !