Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-cracpb1.opb |
MD5SUM | 098fe473d82d5f7d4121673eb775be76 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 26015 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 572 |
Biggest coefficient in the objective function | 5000 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 547769 |
Number of bits of the sum of numbers in the objective function | 20 |
Biggest number in a constraint | 5000 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 547769 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.18 |
Number of variables | 572 |
Total number of constraints | 716 |
Number of constraints which are clauses | 3 |
Number of constraints which are cardinality constraints (but not clauses) | 644 |
Number of constraints which are nor clauses,nor cardinality constraints | 69 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 518 |
LAUNCH ON wulflinc3 THE 2005-09-19 03:05:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2849 boxname=wulflinc3 idbench=505 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 098fe473d82d5f7d4121673eb775be76 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-cracpb1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-cracpb1.opb IDLAUNCH: 2849 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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 : 2 cpu MHz : 451.190 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: 910892 kB Buffers: 35308 kB Cached: 62096 kB SwapCached: 856 kB Active: 65424 kB Inactive: 34624 kB HighTotal: 131008 kB HighFree: 67424 kB LowTotal: 903652 kB LowFree: 843468 kB SwapTotal: 2097136 kB SwapFree: 2095712 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5720 kB Slab: 18104 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:25:39 (client local time) WITH STATUS 10 IN 1207.93 SECONDS stats: 2849 7 1207.93 10
c Parsing PB file... c Converting 215 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################### c -- Clauses(.)/Splits(s): ... c ---[ 214]---> Adder-cost: 1416 maxlim: 2733 bits: 12/12 c ---[ 213]---> Sorter-cost: 634 Base: c ---[ 212]---> Sorter-cost: 238 Base: c ---[ 211]---> Sorter-cost: 238 Base: c ---[ 210]---> Sorter-cost: 206 Base: c ---[ 209]---> Sorter-cost: 356 Base: c ---[ 208]---> Sorter-cost: 356 Base: c ---[ 207]---> Sorter-cost: 264 Base: c ---[ 206]---> Sorter-cost: 126 Base: c ---[ 205]---> Sorter-cost: 356 Base: c ---[ 204]---> Sorter-cost: 106 Base: c ---[ 203]---> BDD-cost: 43 c ---[ 202]---> BDD-cost: 34 c ---[ 201]---> Sorter-cost: 170 Base: c ---[ 200]---> BDD-cost: 29 c ---[ 199]---> Sorter-cost: 180 Base: c ---[ 198]---> BDD-cost: 31 c ---[ 197]---> BDD-cost: 21 c ---[ 195]---> Sorter-cost: 561 Base: c ---[ 193]---> BDD-cost: 41 c ---[ 191]---> Sorter-cost: 255 Base: c ---[ 189]---> Sorter-cost: 207 Base: c ---[ 187]---> Sorter-cost: 491 Base: c ---[ 185]---> Sorter-cost: 239 Base: c ---[ 183]---> Sorter-cost: 281 Base: c ---[ 181]---> Sorter-cost: 181 Base: c ---[ 179]---> Sorter-cost: 291 Base: c ---[ 177]---> Sorter-cost: 127 Base: c ---[ 175]---> BDD-cost: 33 c ---[ 173]---> Sorter-cost: 207 Base: c ---[ 171]---> Sorter-cost: 117 Base: c ---[ 169]---> Sorter-cost: 77 Base: c ---[ 167]---> Sorter-cost: 171 Base: c ---[ 165]---> Sorter-cost: 127 Base: c ---[ 163]---> BDD-cost: 29 c ---[ 161]---> BDD-cost: 25 c ---[ 159]---> Adder-cost: 155 maxlim: 27 bits: 6/5 c ---[ 157]---> Sorter-cost: 631 Base: c ---[ 155]---> Sorter-cost: 689 Base: c ---[ 153]---> Sorter-cost: 609 Base: c ---[ 151]---> Sorter-cost: 971 Base: c ---[ 149]---> Sorter-cost: 991 Base: c ---[ 147]---> Sorter-cost: 755 Base: c ---[ 145]---> Sorter-cost: 371 Base: c ---[ 143]---> Sorter-cost: 927 Base: c ---[ 141]---> Sorter-cost: 355 Base: c ---[ 139]---> Sorter-cost: 313 Base: c ---[ 137]---> Sorter-cost: 279 Base: c ---[ 135]---> Sorter-cost: 501 Base: c ---[ 133]---> Sorter-cost: 225 Base: c ---[ 131]---> Sorter-cost: 517 Base: c ---[ 129]---> Sorter-cost: 197 Base: c ---[ 127]---> BDD-cost: 66 c ---[ 126]---> Adder-cost: 732 maxlim: 1601 bits: 12/11 c ---[ 125]---> Adder-cost: 1184 maxlim: 406 bits: 10/9 c ---[ 124]---> Adder-cost: 255 maxlim: 863 bits: 11/10 c ---[ 123]---> BDD-cost: 27 c ---[ 122]---> BDD-cost: 35 c ---[ 121]---> Sorter-cost: 172 Base: c ---[ 120]---> BDD-cost: 31 c ---[ 118]---> BDD-cost: 51 c ---[ 115]---> BDD-cost: 80 c ---[ 114]---> Sorter-cost: 238 Base: c ---[ 113]---> Sorter-cost: 478 Base: c ---[ 112]---> Sorter-cost: 254 Base: c ---[ 111]---> BDD-cost: 21 c ---[ 110]---> Sorter-cost: 474 Base: c ---[ 109]---> BDD-cost: 29 c ---[ 108]---> BDD-cost: 23 c ---[ 106]---> BDD-cost: 16 c ---[ 104]---> BDD-cost: 17 c ---[ 102]---> BDD-cost: 5 c ---[ 100]---> BDD-cost: 43 c ---[ 98]---> BDD-cost: 92 c ---[ 96]---> BDD-cost: 183 c ---[ 94]---> BDD-cost: 11 c ---[ 92]---> BDD-cost: 29 c ---[ 90]---> BDD-cost: 29 c ---[ 88]---> BDD-cost: 19 c ---[ 86]---> BDD-cost: 11 c ---[ 84]---> BDD-cost: 11 c ---[ 82]---> BDD-cost: 31 c ---[ 80]---> BDD-cost: 23 c ---[ 78]---> BDD-cost: 7 c ---[ 76]---> BDD-cost: 13 c ---[ 74]---> BDD-cost: 14 c ---[ 72]---> BDD-cost: 38 c ---[ 70]---> BDD-cost: 23 c ---[ 68]---> BDD-cost: 35 c ---[ 66]---> BDD-cost: 37 c ---[ 64]---> BDD-cost: 7 c ---[ 62]---> BDD-cost: 17 c ---[ 60]---> BDD-cost: 17 c ---[ 58]---> BDD-cost: 43 c ---[ 56]---> BDD-cost: 11 c ---[ 54]---> BDD-cost: 29 c ---[ 52]---> BDD-cost: 7 c ---[ 50]---> BDD-cost: 16 c ---[ 48]---> BDD-cost: 24 c ---[ 46]---> BDD-cost: 5 c ---[ 44]---> BDD-cost: 14 c ---[ 42]---> BDD-cost: 11 c ---[ 40]---> BDD-cost: 13 c ---[ 38]---> BDD-cost: 16 c ---[ 36]---> BDD-cost: 19 c ---[ 34]---> BDD-cost: 14 c ---[ 32]---> BDD-cost: 19 c ---[ 30]---> BDD-cost: 11 c ---[ 28]---> BDD-cost: 4 c ---[ 26]---> BDD-cost: 11 c ---[ 24]---> BDD-cost: 14 c ---[ 22]---> BDD-cost: 15 c ---[ 20]---> BDD-cost: 48 c ---[ 18]---> BDD-cost: 51 c ---[ 16]---> BDD-cost: 11 c ---[ 14]---> BDD-cost: 6 c ---[ 12]---> BDD-cost: 51 c ---[ 10]---> BDD-cost: 8 c ---[ 8]---> BDD-cost: 14 c ---[ 6]---> BDD-cost: 43 c ---[ 4]---> BDD-cost: 31 c ---[ 2]---> BDD-cost: 22 c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 59268 172692 | 19756 0 0 nan | 0.000 % | c | 100 | 58967 172015 | 21731 54 378 7.0 | 2.982 % | c | 250 | 58871 171801 | 23904 194 2163 11.1 | 3.144 % | c | 478 | 58643 171296 | 26295 390 6723 17.2 | 3.542 % | c | 817 | 58486 170918 | 28924 712 11817 16.6 | 3.778 % | c | 1326 | 58486 170918 | 31817 1221 20748 17.0 | 3.778 % | c | 2085 | 58029 169847 | 34998 1939 28436 14.7 | 4.505 % | c | 3226 | 57206 167973 | 38498 2938 45487 15.5 | 5.901 % | c | 4935 | 56852 167094 | 42348 4588 80961 17.6 | 6.397 % | c | 7501 | 55779 164665 | 46583 6967 212735 30.5 | 8.306 % | c | 11348 | 55700 164452 | 51241 10794 356680 33.0 | 8.428 % | c | 17115 | 55398 163695 | 56366 16515 718991 43.5 | 8.872 % | c | 25765 | 54846 162412 | 62002 25097 1273366 50.7 | 9.875 % | c | 38739 | 54722 162120 | 68203 38032 2543822 66.9 | 10.083 % | c | 58200 | 54453 161440 | 75023 57412 4736486 82.5 | 10.481 % | c | 87392 | 54220 160887 | 82525 18335 2211078 120.6 | 10.885 % | c | 131185 | 53722 159704 | 90778 62096 8034036 129.4 | 11.710 % | c ============================================================================== c [1mFound solution: 72848[0m c ---[ 0]---> Adder-cost: 4504 maxlim: 473010 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137357 | 84969 271519 | 28323 68249 8557934 125.4 | 11.710 % | c | 137457 | 84969 271519 | 31155 18289 1526343 83.5 | 9.573 % | c | 137608 | 84969 271519 | 34270 18440 1531269 83.0 | 9.573 % | c | 137833 | 84969 271519 | 37697 18665 1540508 82.5 | 9.573 % | c | 138173 | 84969 271519 | 41467 19005 1552871 81.7 | 9.573 % | c | 138679 | 84969 271519 | 45614 19511 1569702 80.5 | 9.573 % | c | 139438 | 84897 271358 | 50175 20263 1642598 81.1 | 9.669 % | c | 140578 | 84809 271158 | 55193 21391 1698960 79.4 | 9.797 % | c | 142286 | 84638 270736 | 60712 23085 1760646 76.3 | 9.989 % | c | 144851 | 84610 270643 | 66784 25646 1921260 74.9 | 10.003 % | c | 148695 | 84610 270643 | 73462 29490 2086893 70.8 | 10.003 % | c | 154464 | 84557 270524 | 80808 35250 2416240 68.5 | 10.072 % | c | 163115 | 84531 270467 | 88889 43897 3145277 71.7 | 10.104 % | c | 176093 | 84489 270353 | 97778 56863 4179607 73.5 | 10.145 % | c | 195554 | 84380 270057 | 107556 76306 5512864 72.2 | 10.273 % | c | 224747 | 84133 269463 | 118312 105473 8398966 79.6 | 10.598 % | c | 268536 | 83772 268630 | 130143 47858 3799427 79.4 | 11.092 % | c | 334220 | 83640 268329 | 143157 113532 12757707 112.4 | 11.262 % | c c *** TERMINATED *** s SATISFIABLE v -GPT00001_bit0 -GPT00002_bit0 -GPT00003_bit0 -GPT00004_bit0 -GPT00005_bit0 -GPT00006_bit0 -GPT00007_bit0 -GPT00008_bit0 -GPT00009_bit0 -GPT00010_bit0 -GPT00011_bit0 -GPT00012_bit0 -GPT00013_bit0 -GPT00014_bit0 -GPT00015_bit0 -GPT00016_bit0 -GPT00017_bit0 -GPT00018_bit0 -GPT00019_bit0 -GPT00020_bit0 -GPT00021_bit0 -GPT00022_bit0 -GPT00023_bit0 -GPT00024_bit0 -GPT00025_bit0 GPT00026_bit0 -GPT00027_bit0 GPT00028_bit0 -GPT00029_bit0 -GPT00030_bit0 -GPT00031_bit0 -GPT00032_bit0 -GPT00033_bit0 GPT00034_bit0 -GPT00035_bit0 -GPT00036_bit0 -GPT00037_bit0 GPT00038_bit0 -GPT00039_bit0 -GPT00040_bit0 -GPT00041_bit0 -GPT00042_bit0 -GPT00043_bit0 -GPT00044_bit0 -GPT00045_bit0 -GPT00046_bit0 -GPT00047_bit0 -GPT00048_bit0 -GPT00049_bit0 -GPT00050_bit0 GPT00051_bit0 -GPT00052_bit0 GPT00053_bit0 -GPT00054_bit0 -GPT00055_bit0 -GPT00056_bit0 -GPT00057_bit0 -GPT00058_bit0 GPT00059_bit0 -GPT00060_bit0 -GPT00061_bit0 -GPT00062_bit0 -GPT00063_bit0 -GPT00064_bit0 -GPT00065_bit0 -GPT00066_bit0 -GPT00067_bit0 -GPT00068_bit0 -GPT00069_bit0 GPT00070_bit0 -GPT00071_bit0 -GPT00072_bit0 -GPT00073_bit0 -GPT00074_bit0 -GPT00075_bit0 -GPT00076_bit0 -GPT00077_bit0 -GPT00078_bit0 -GPT00079_bit0 -GPT00080_bit0 -GPT00081_bit0 -GPT00082_bit0 -GPT00083_bit0 GPT00084_bit0 -GPT00085_bit0 -GPT00086_bit0 -GPT00087_bit0 -GPT00088_bit0 -GPT00089_bit0 -GPT00090_bit0 -GPT00091_bit0 -GPT00092_bit0 -GPT00093_bit0 -GPT00094_bit0 -GPT00095_bit0 -GPT00096_bit0 -GPT00097_bit0 -GPT00098_bit0 -GPT00099_bit0 -GPT00100_bit0 -GPT00101_bit0 -GPT00102_bit0 -GPT00103_bit0 -GPT00104_bit0 -GPT00105_bit0 -GPT00106_bit0 -GPT00107_bit0 -GPT00108_bit0 -GPT00109_bit0 -GPT00110_bit0 -GPT00111_bit0 GPT00112_bit0 -GPT00113_bit0 -GPT00114_bit0 -GPT00115_bit0 -GPT00116_bit0 GPT00117_bit0 -GPT00118_bit0 -GPT00119_bit0 -GPT00120_bit0 -GPT00121_bit0 -GPT00122_bit0 GPT00123_bit0 GPT00124_bit0 -GPT00125_bit0 -GPT00126_bit0 -GPT00127_bit0 GPT00128_bit0 -GPT00129_bit0 GPT00130_bit0 -GPT00131_bit0 -GPT00132_bit0 -GPT00133_bit0 -GPT00134_bit0 -GPT00135_bit0 GPT00136_bit0 -GPT00137_bit0 -GPT00138_bit0 -GPT00139_bit0 -GPT00140_bit0 -GPT00141_bit0 GPT00142_bit0 -GPT00143_bit0 -GPT00144_bit0 -GPT00145_bit0 -GPT00146_bit0 -GPT00147_bit0 -GPT00148_bit0 -GPT00149_bit0 -GPT00150_bit0 -GPT00151_bit0 -GPT00152_bit0 -GPT00153_bit0 -GPT00154_bit0 -GPT00155_bit0 -GPT00156_bit0 -GPT00157_bit0 -GPT00158_bit0 -GPT00159_bit0 -GPT00160_bit0 -GPT00161_bit0 -GPT00162_bit0 -GPT00163_bit0 -GPT00164_bit0 -GPT00165_bit0 -GPT00166_bit0 -GPT00167_bit0 -GPT00168_bit0 -GPT00169_bit0 -GPT00170_bit0 -GPT00171_bit0 -GPT00172_bit0 -GPT00173_bit0 -GPT00174_bit0 -GPT00175_bit0 -GPT00176_bit0 -GPT00177_bit0 -GPT00178_bit0 -GPT00179_bit0 -GPT00180_bit0 -GPT00181_bit0 -GPT00182_bit0 -GPT00183_bit0 -GPT00184_bit0 GPT00185_bit0 -GPT00186_bit0 -GPT00187_bit0 -GPT00188_bit0 -GPT00189_bit0 -GPT00190_bit0 -GPT00191_bit0 -GPT00192_bit0 -GPT00193_bit0 -GPT00194_bit0 GPT00195_bit0 -GPT00196_bit0 -GPT00197_bit0 -GPT00198_bit0 -GPT00199_bit0 -GPT00200_bit0 -GPT00201_bit0 -GPT00202_bit0 -GPT00203_bit0 -GPT00204_bit0 -GPT00205_bit0 -GPT00206_bit0 -GPT00207_bit0 -GPT00208_bit0 -GPT00209_bit0 -GPT00210_bit0 -GPT00211_bit0 -GPT00212_bit0 -GPT00213_bit0 -GPT00214_bit0 -GPT00215_bit0 -GPT00216_bit0 -GPT00217_bit0 -GPT00218_bit0 GPT00219_bit0 -GPT00220_bit0 -GPT00221_bit0 -GPT00222_bit0 -GPT00223_bit0 -GPT00224_bit0 -GPT00225_bit0 -GPT00226_bit0 -GPT00227_bit0 -GPT00228_bit0 -GPT00229_bit0 -GPT00230_bit0 -GPT00231_bit0 GPT00232_bit0 -GPT00233_bit0 -GPT00234_bit0 -GPT00235_bit0 -GPT00236_bit0 -GPT00237_bit0 -GPT00238_bit0 -GPT00239_bit0 -GPT00240_bit0 -GPT00241_bit0 -GPT00242_bit0 -GPT00243_bit0 -GPT00244_bit0 -GPT00245_bit0 -GPT00246_bit0 -GPT00247_bit0 -GPT00248_bit0 -GPT00249_bit0 -GPT00250_bit0 GPT00251_bit0 -GPT00252_bit0 -GPT00253_bit0 -GPT00254_bit0 -GPT00255_bit0 -GPT00256_bit0 -GPT00257_bit0 GPT00258_bit0 -GPT00259_bit0 -GPT00260_bit0 -GPT00261_bit0 -GPT00262_bit0 -GPT00263_bit0 -GPT00264_bit0 -GPT00265_bit0 GPT00266_bit0 -GPT00267_bit0 -GPT00268_bit0 -GPT00269_bit0 -GPT00270_bit0 -GPT00271_bit0 -GPT00272_bit0 -GPT00273_bit0 -GPT00274_bit0 -GPT00275_bit0 -GPT00276_bit0 -GPT00277_bit0 GPT00278_bit0 -GPT00279_bit0 -GPT00280_bit0 -GPT00281_bit0 -GPT00282_bit0 -GPT00283_bit0 -GPT00284_bit0 -GPT00285_bit0 -GPT00286_bit0 -GPT00287_bit0 GPT00288_bit0 -GPT00289_bit0 GPT00290_bit0 -GPT00291_bit0 GPT00292_bit0 -GPT00293_bit0 -GPT00294_bit0 -GPT00295_bit0 -GPT00296_bit0 -GPT00297_bit0 -GPT00298_bit0 -GPT00299_bit0 -GPT00300_bit0 -GPT00301_bit0 -GPT00302_bit0 -GPT00303_bit0 -GPT00304_bit0 -GPT00305_bit0 -GPT00306_bit0 -GPT00307_bit0 -GPT00308_bit0 -GPT00309_bit0 -GPT00310_bit0 -GPT00311_bit0 -GPT00312_bit0 -GPT00313_bit0 -GPT00314_bit0 -GPT00315_bit0 -GPT00316_bit0 -GPT00317_bit0 -GPT00318_bit0 GPT00319_bit0 -GPT00320_bit0 -GPT00321_bit0 -GPT00322_bit0 -GPT00323_bit0 -GPT00324_bit0 -GPT00325_bit0 -GPT00326_bit0 -GPT00327_bit0 -GPT00328_bit0 -GPT00329_bit0 -GPT00330_bit0 -GPT00331_bit0 -GPT00332_bit0 -GPT00333_bit0 -GPT00334_bit0 -GPT00335_bit0 -GPT00336_bit0 -GPT00337_bit0 -GPT00338_bit0 -GPT00339_bit0 -GPT00340_bit0 -GPT00341_bit0 -GPT00342_bit0 -GPT00343_bit0 -GPT00344_bit0 -GPT00345_bit0 -GPT00346_bit0 -GPT00347_bit0 -GPT00348_bit0 -GPT00349_bit0 -GPT00350_bit0 -GPT00351_bit0 -GPT00352_bit0 -GPT00353_bit0 -GPT00354_bit0 -GPT00355_bit0 -GPT00356_bit0 GPT00357_bit0 -GPT00358_bit0 -GPT00359_bit0 GPT00360_bit0 -GPT00361_bit0 -GPT00362_bit0 GPT00363_bit0 -GPT00364_bit0 -GPT00365_bit0 -GPT00366_bit0 -GPT00367_bit0 -GPT00368_bit0 -GPT00369_bit0 -GPT00370_bit0 -GPT00371_bit0 -GPT00372_bit0 -GPT00373_bit0 -GPT00374_bit0 -GPT00375_bit0 -GPT00376_bit0 -GPT00377_bit0 -GPT00378_bit0 -GPT00379_bit0 -GPT00380_bit0 -GPT00381_bit0 -GPT00382_bit0 -GPT00383_bit0 GPT00384_bit0 GPT00385_bit0 -GPT00386_bit0 -GPT00387_bit0 GPT00388_bit0 -GPT00389_bit0 -GPT00390_bit0 -GPT00391_bit0 -GPT00392_bit0 -GPT00393_bit0 -GPT00394_bit0 -GPT00395_bit0 -GPT00396_bit0 -GPT00397_bit0 -GPT00398_bit0 -GPT00399_bit0 -GPT00400_bit0 -GPT00401_bit0 -GPT00402_bit0 -GPT00403_bit0 -GPT00404_bit0 -GPT00405_bit0 -GPT00406_bit0 -GPT00407_bit0 -GPT00408_bit0 -GPT00409_bit0 -GPT00410_bit0 -GPT00411_bit0 -GPT00412_bit0 -GPT00413_bit0 GPT00414_bit0 -GPT00415_bit0 -GPT00416_bit0 -GPT00417_bit0 GPT00418_bit0 -GPT00419_bit0 -GPT00420_bit0 -GPT00421_bit0 -GPT00422_bit0 -GPT00423_bit0 -GPT00424_bit0 -GPT00425_bit0 -GPT00426_bit0 -GPT00427_bit0 -GPT00428_bit0 -GPT00429_bit0 -GPT00430_bit0 -GPT00431_bit0 -GPT00432_bit0 -GPT00433_bit0 -GPT00434_bit0 -GPT00435_bit0 -GPT00436_bit0 -GPT00437_bit0 -GPT00438_bit0 -GPT00439_bit0 -GPT00440_bit0 -GPT00441_bit0 -GPT00442_bit0 -GPT00443_bit0 GPT00444_bit0 -GPT00445_bit0 -GPT00446_bit0 -GPT00447_bit0 -GPT00448_bit0 -GPT00449_bit0 -GPT00450_bit0 -GPT00451_bit0 -GPT00452_bit0 -GPT00453_bit0 GPT00454_bit0 -GPT00455_bit0 -GPT00456_bit0 -GPT00457_bit0 -GPT00458_bit0 -GPT00459_bit0 -GPT00460_bit0 -GPT00461_bit0 -GPT00462_bit0 -GPT00463_bit0 -GPT00464_bit0 -GPT00465_bit0 -GPT00466_bit0 -GPT00467_bit0 -GPT00468_bit0 -GPT00469_bit0 -GPT00470_bit0 -GPT00471_bit0 -GPT00472_bit0 -GPT00473_bit0 -GPT00474_bit0 -GPT00475_bit0 -GPT00476_bit0 GPT00477_bit0 -GPT00478_bit0 -GPT00479_bit0 -GPT00480_bit0 -GPT00481_bit0 -GPT00482_bit0 -GPT00483_bit0 -GPT00484_bit0 -GPT00485_bit0 -GPT00486_bit0 -GPT00487_bit0 -GPT00488_bit0 -GPT00489_bit0 -GPT00490_bit0 -GPT00491_bit0 -GPT00492_bit0 -GPT00493_bit0 -GPT00494_bit0 -GPT00495_bit0 -GPT00496_bit0 -GPT00497_bit0 -GPT00498_bit0 -GPT00499_bit0 -GPT00500_bit0 -GPT00501_bit0 -GPT00502_bit0 -GPT00503_bit0 -GPT00504_bit0 -GPT00505_bit0 -GPT00506_bit0 -GPT00507_bit0 -GPT00508_bit0 -GPT00509_bit0 -GPT00510_bit0 -GPT00511_bit0 -GPT00512_bit0 -GPT00513_bit0 -GPT00514_bit0 -GPT00515_bit0 -GPT00516_bit0 -GPT00517_bit0 -GPT00518_bit0 -ECAR0001_bit0 -ECAR0002_bit0 ECAR0003_bit0 -ECAR0004_bit0 -ECAR0005_bit0 -ECAR0006_bit0 -ECAR0007_bit0 -ECAR0008_bit0 -ECAR0009_bit0 ECAR0010_bit0 -ECAR0011_bit0 ECAR0012_bit0 -ECAR0013_bit0 ECAR0014_bit0 -ECAR0015_bit0 -ECAR0016_bit0 -ECAR0017_bit0 -ECAR0018_bit0 -ECAR0019_bit0 -ECAR0020_bit0 ECAR0021_bit0 -ECAR0022_bit0 -ECAR0023_bit0 ECAR0024_bit0 -ECAR0025_bit0 -ECAR0026_bit0 -ECAR0027_bit0 -ECAR0028_bit0 -ECAR002
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/24384/stat): 24384 (minisat+_script) R 24383 24384 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788279559 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24384/statm): 174 3 169 147 0 27 0 [pid=24384] 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=24385 New process pid=24386 New process pid=24387 execve syscall for /bin/sed executable 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 One traced child (pid=24386) exited with status: 0 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=24387) exited with status: 0 One traced child (pid=24385) exited with status: 0 New process pid=24388 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-cracpb1.opb [startup+10.0041 s] Raw data (loadavg): 0.72 0.88 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 2159 0 0 0 976 10 0 0 25 0 1 0 1788279564 9793536 2050 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 2391 2050 145 145 0 2246 0 [pid=24388] vsize: 9564 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 11688 [startup+20.0049 s] Raw data (loadavg): 0.76 0.88 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 2520 0 0 0 1967 12 0 0 25 0 1 0 1788279564 11280384 2411 4294967295 134512640 135094434 3221224432 3221223148 134561654 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 2754 2411 145 145 0 2609 0 [pid=24388] vsize: 11016 Current children cumulated CPU time (s) 19.81 Current children cumulated vsize (Kb) 13140 [startup+30.0057 s] Raw data (loadavg): 0.87 0.90 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 3176 0 0 0 2959 15 0 0 25 0 1 0 1788279564 13996032 3067 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 3417 3067 145 145 0 3272 0 [pid=24388] vsize: 13668 Current children cumulated CPU time (s) 29.76 Current children cumulated vsize (Kb) 15792 [startup+40.0056 s] Raw data (loadavg): 0.89 0.91 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 3546 0 0 0 3953 17 0 0 25 0 1 0 1788279564 15491072 3437 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 3782 3437 145 145 0 3637 0 [pid=24388] vsize: 15128 Current children cumulated CPU time (s) 39.72 Current children cumulated vsize (Kb) 17252 [startup+50.0074 s] Raw data (loadavg): 0.91 0.91 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 4303 0 0 0 4941 22 0 0 25 0 1 0 1788279564 18690048 4194 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 4563 4194 145 145 0 4418 0 [pid=24388] vsize: 18252 Current children cumulated CPU time (s) 49.65 Current children cumulated vsize (Kb) 20376 [startup+60.0082 s] Raw data (loadavg): 0.92 0.91 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 4992 0 0 0 5929 26 0 0 25 0 1 0 1788279564 21495808 4883 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 5248 4883 145 145 0 5103 0 [pid=24388] vsize: 20992 Current children cumulated CPU time (s) 59.57 Current children cumulated vsize (Kb) 23116 [startup+70.0091 s] Raw data (loadavg): 0.93 0.91 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 5340 0 0 0 6923 30 0 0 25 0 1 0 1788279564 22908928 5231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 5593 5231 145 145 0 5448 0 [pid=24388] vsize: 22372 Current children cumulated CPU time (s) 69.55 Current children cumulated vsize (Kb) 24496 [startup+80.0109 s] Raw data (loadavg): 0.94 0.92 0.96 1/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) T 24384 24384 31915 0 -1 0 5846 0 0 0 7912 33 0 0 25 0 1 0 1788279564 24965120 5737 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/24388/statm): 6095 5737 145 145 0 5950 0 [pid=24388] vsize: 24380 Current children cumulated CPU time (s) 79.47 Current children cumulated vsize (Kb) 26504 [startup+90.0118 s] Raw data (loadavg): 0.95 0.92 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 6413 0 0 0 8900 38 0 0 25 0 1 0 1788279564 27267072 6304 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 6657 6304 145 145 0 6512 0 [pid=24388] vsize: 26628 Current children cumulated CPU time (s) 89.4 Current children cumulated vsize (Kb) 28752 [startup+100.013 s] Raw data (loadavg): 0.96 0.92 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 7019 0 0 0 9889 42 0 0 25 0 1 0 1788279564 29732864 6910 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 7259 6910 145 145 0 7114 0 [pid=24388] vsize: 29036 Current children cumulated CPU time (s) 99.33 Current children cumulated vsize (Kb) 31160 [startup+110.013 s] Raw data (loadavg): 0.96 0.92 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) T 24384 24384 31915 0 -1 0 7407 0 0 0 10882 45 0 0 25 0 1 0 1788279564 31313920 7298 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/24388/statm): 7645 7298 145 145 0 7500 0 [pid=24388] vsize: 30580 Current children cumulated CPU time (s) 109.29 Current children cumulated vsize (Kb) 32704 [startup+120.014 s] Raw data (loadavg): 0.97 0.92 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 7841 0 0 0 11873 49 0 0 25 0 1 0 1788279564 33083392 7732 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 8077 7732 145 145 0 7932 0 [pid=24388] vsize: 32308 Current children cumulated CPU time (s) 119.24 Current children cumulated vsize (Kb) 34432 [startup+130.015 s] Raw data (loadavg): 0.97 0.93 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 8299 0 0 0 12865 53 0 0 25 0 1 0 1788279564 35205120 8190 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 8595 8190 145 145 0 8450 0 [pid=24388] vsize: 34380 Current children cumulated CPU time (s) 129.2 Current children cumulated vsize (Kb) 36504 [startup+140.016 s] Raw data (loadavg): 0.98 0.93 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 8760 0 0 0 13856 56 0 0 25 0 1 0 1788279564 37085184 8651 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 9054 8651 145 145 0 8909 0 [pid=24388] vsize: 36216 Current children cumulated CPU time (s) 139.14 Current children cumulated vsize (Kb) 38340 [startup+150.017 s] Raw data (loadavg): 0.98 0.93 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 9201 0 0 0 14849 59 0 0 25 0 1 0 1788279564 38875136 9092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 9491 9092 145 145 0 9346 0 [pid=24388] vsize: 37964 Current children cumulated CPU time (s) 149.1 Current children cumulated vsize (Kb) 40088 [startup+160.018 s] Raw data (loadavg): 0.98 0.93 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 9654 0 0 0 15841 62 0 0 25 0 1 0 1788279564 40726528 9545 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 9943 9545 145 145 0 9798 0 [pid=24388] vsize: 39772 Current children cumulated CPU time (s) 159.05 Current children cumulated vsize (Kb) 41896 [startup+170.018 s] Raw data (loadavg): 0.98 0.93 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 10107 0 0 0 16834 65 0 0 25 0 1 0 1788279564 42569728 9998 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 10393 9998 145 145 0 10248 0 [pid=24388] vsize: 41572 Current children cumulated CPU time (s) 169.01 Current children cumulated vsize (Kb) 43696 [startup+180.019 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 10554 0 0 0 17826 69 0 0 25 0 1 0 1788279564 44396544 10445 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 10839 10445 145 145 0 10694 0 [pid=24388] vsize: 43356 Current children cumulated CPU time (s) 178.97 Current children cumulated vsize (Kb) 45480 [startup+190.02 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 10941 0 0 0 18818 73 0 0 25 0 1 0 1788279564 45989888 10832 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 11228 10832 145 145 0 11083 0 [pid=24388] vsize: 44912 Current children cumulated CPU time (s) 188.93 Current children cumulated vsize (Kb) 47036 [startup+200.022 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11328 0 0 0 19809 77 0 0 25 0 1 0 1788279564 47579136 11219 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 11616 11219 145 145 0 11471 0 [pid=24388] vsize: 46464 Current children cumulated CPU time (s) 198.88 Current children cumulated vsize (Kb) 48588 [startup+210.023 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11729 0 0 0 20802 81 0 0 25 0 1 0 1788279564 49229824 11620 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12019 11620 145 145 0 11874 0 [pid=24388] vsize: 48076 Current children cumulated CPU time (s) 208.85 Current children cumulated vsize (Kb) 50200 [startup+220.024 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 21800 82 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 218.84 Current children cumulated vsize (Kb) 50544 [startup+230.024 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 22800 82 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 228.84 Current children cumulated vsize (Kb) 50544 [startup+240.025 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 23799 83 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 238.84 Current children cumulated vsize (Kb) 50544 [startup+250.027 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 24799 84 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 248.85 Current children cumulated vsize (Kb) 50544 [startup+260.029 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 25798 84 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 258.84 Current children cumulated vsize (Kb) 50544 [startup+270.029 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 26798 85 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 268.85 Current children cumulated vsize (Kb) 50544 [startup+280.03 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 27797 86 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 278.85 Current children cumulated vsize (Kb) 50544 [startup+290.031 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 28796 86 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 288.84 Current children cumulated vsize (Kb) 50544 [startup+300.031 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 29796 87 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 298.85 Current children cumulated vsize (Kb) 50544 [startup+310.032 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 30795 87 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 308.84 Current children cumulated vsize (Kb) 50544 [startup+320.033 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 31795 88 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223104 134556239 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 318.85 Current children cumulated vsize (Kb) 50544 [startup+330.034 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11816 0 0 0 32794 89 0 0 25 0 1 0 1788279564 49582080 11707 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11707 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 328.85 Current children cumulated vsize (Kb) 50544 [startup+340.035 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11817 0 0 0 33794 89 0 0 25 0 1 0 1788279564 49582080 11708 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11708 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 338.85 Current children cumulated vsize (Kb) 50544 [startup+350.036 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 11817 0 0 0 34793 90 0 0 25 0 1 0 1788279564 49582080 11708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 12105 11708 145 145 0 11960 0 [pid=24388] vsize: 48420 Current children cumulated CPU time (s) 348.85 Current children cumulated vsize (Kb) 50544 [startup+360.036 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 35780 99 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 358.81 Current children cumulated vsize (Kb) 58860 [startup+370.037 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 36779 99 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 368.8 Current children cumulated vsize (Kb) 58860 [startup+380.039 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 37779 100 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223024 134551718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 378.81 Current children cumulated vsize (Kb) 58860 [startup+390.04 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 38778 100 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 388.8 Current children cumulated vsize (Kb) 58860 [startup+400.042 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 39778 100 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 398.8 Current children cumulated vsize (Kb) 58860 [startup+410.043 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 40778 101 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 408.81 Current children cumulated vsize (Kb) 58860 [startup+420.042 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 41777 102 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 418.81 Current children cumulated vsize (Kb) 58860 [startup+430.044 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 42777 102 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 428.81 Current children cumulated vsize (Kb) 58860 [startup+440.045 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 43777 102 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 438.81 Current children cumulated vsize (Kb) 58860 [startup+450.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 44776 103 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 448.81 Current children cumulated vsize (Kb) 58860 [startup+460.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 45776 103 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 458.81 Current children cumulated vsize (Kb) 58860 [startup+470.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14416 0 0 0 46777 103 0 0 25 0 1 0 1788279564 58097664 13729 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13729 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 468.82 Current children cumulated vsize (Kb) 58860 [startup+480.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14417 0 0 0 47777 103 0 0 25 0 1 0 1788279564 58097664 13730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13730 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 478.82 Current children cumulated vsize (Kb) 58860 [startup+490.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14417 0 0 0 48777 103 0 0 25 0 1 0 1788279564 58097664 13730 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13730 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 488.82 Current children cumulated vsize (Kb) 58860 [startup+500.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14417 0 0 0 49777 103 0 0 25 0 1 0 1788279564 58097664 13730 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13730 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 498.82 Current children cumulated vsize (Kb) 58860 [startup+510.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14417 0 0 0 50778 103 0 0 25 0 1 0 1788279564 58097664 13730 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13730 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 508.83 Current children cumulated vsize (Kb) 58860 [startup+520.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14417 0 0 0 51778 103 0 0 25 0 1 0 1788279564 58097664 13730 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13730 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 518.83 Current children cumulated vsize (Kb) 58860 [startup+530.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14419 0 0 0 52778 103 0 0 25 0 1 0 1788279564 58097664 13732 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13732 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 528.83 Current children cumulated vsize (Kb) 58860 [startup+540.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14422 0 0 0 53778 103 0 0 25 0 1 0 1788279564 58097664 13735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13735 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 538.83 Current children cumulated vsize (Kb) 58860 [startup+550.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14425 0 0 0 54779 103 0 0 25 0 1 0 1788279564 58097664 13738 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13738 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 548.84 Current children cumulated vsize (Kb) 58860 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14427 0 0 0 55779 103 0 0 25 0 1 0 1788279564 58097664 13740 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13740 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 558.84 Current children cumulated vsize (Kb) 58860 [startup+570.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14432 0 0 0 56779 103 0 0 25 0 1 0 1788279564 58097664 13745 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13745 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 568.84 Current children cumulated vsize (Kb) 58860 [startup+580.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14434 0 0 0 57779 103 0 0 25 0 1 0 1788279564 58097664 13747 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14184 13747 145 145 0 14039 0 [pid=24388] vsize: 56736 Current children cumulated CPU time (s) 578.84 Current children cumulated vsize (Kb) 58860 [startup+590.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14686 0 0 0 58775 105 0 0 25 0 1 0 1788279564 59121664 13999 4294967295 134512640 135094434 3221224432 3221223104 134556331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14434 13999 145 145 0 14289 0 [pid=24388] vsize: 57736 Current children cumulated CPU time (s) 588.82 Current children cumulated vsize (Kb) 59860 [startup+600.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 14851 0 0 0 59772 106 0 0 25 0 1 0 1788279564 59789312 14164 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14597 14164 145 145 0 14452 0 [pid=24388] vsize: 58388 Current children cumulated CPU time (s) 598.8 Current children cumulated vsize (Kb) 60512 [startup+610.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 15090 0 0 0 60767 107 0 0 25 0 1 0 1788279564 60768256 14403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 14836 14403 145 145 0 14691 0 [pid=24388] vsize: 59344 Current children cumulated CPU time (s) 608.76 Current children cumulated vsize (Kb) 61468 [startup+620.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 15369 0 0 0 61763 109 0 0 25 0 1 0 1788279564 61902848 14682 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 15113 14682 145 145 0 14968 0 [pid=24388] vsize: 60452 Current children cumulated CPU time (s) 618.74 Current children cumulated vsize (Kb) 62576 [startup+630.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 15731 0 0 0 62757 111 0 0 25 0 1 0 1788279564 63389696 15044 4294967295 134512640 135094434 3221224432 3221223100 134555968 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 15476 15044 145 145 0 15331 0 [pid=24388] vsize: 61904 Current children cumulated CPU time (s) 628.7 Current children cumulated vsize (Kb) 64028 [startup+640.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16011 0 0 0 63752 114 0 0 25 0 1 0 1788279564 64524288 15324 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 15753 15324 145 145 0 15608 0 [pid=24388] vsize: 63012 Current children cumulated CPU time (s) 638.68 Current children cumulated vsize (Kb) 65136 [startup+650.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16151 0 0 0 64750 114 0 0 25 0 1 0 1788279564 65085440 15464 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 15890 15464 145 145 0 15745 0 [pid=24388] vsize: 63560 Current children cumulated CPU time (s) 648.66 Current children cumulated vsize (Kb) 65684 [startup+660.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16330 0 0 0 65747 115 0 0 25 0 1 0 1788279564 65810432 15643 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16067 15643 145 145 0 15922 0 [pid=24388] vsize: 64268 Current children cumulated CPU time (s) 658.64 Current children cumulated vsize (Kb) 66392 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16524 0 0 0 66744 117 0 0 25 0 1 0 1788279564 66596864 15837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16259 15837 145 145 0 16114 0 [pid=24388] vsize: 65036 Current children cumulated CPU time (s) 668.63 Current children cumulated vsize (Kb) 67160 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 67744 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 678.63 Current children cumulated vsize (Kb) 67248 [startup+690.067 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 68744 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 688.63 Current children cumulated vsize (Kb) 67248 [startup+700.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 69744 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 698.63 Current children cumulated vsize (Kb) 67248 [startup+710.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 70744 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 708.63 Current children cumulated vsize (Kb) 67248 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 71745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 718.64 Current children cumulated vsize (Kb) 67248 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 72745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 728.64 Current children cumulated vsize (Kb) 67248 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 73745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 738.64 Current children cumulated vsize (Kb) 67248 [startup+750.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 74745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 748.64 Current children cumulated vsize (Kb) 67248 [startup+760.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 75745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 758.64 Current children cumulated vsize (Kb) 67248 [startup+770.075 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 76745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 768.64 Current children cumulated vsize (Kb) 67248 [startup+780.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 77745 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 778.64 Current children cumulated vsize (Kb) 67248 [startup+790.077 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 78746 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 788.65 Current children cumulated vsize (Kb) 67248 [startup+800.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 79746 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 798.65 Current children cumulated vsize (Kb) 67248 [startup+810.081 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 80747 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 808.66 Current children cumulated vsize (Kb) 67248 [startup+820.082 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 81747 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 818.66 Current children cumulated vsize (Kb) 67248 [startup+830.084 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 82747 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 828.66 Current children cumulated vsize (Kb) 67248 [startup+840.085 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 83747 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 838.66 Current children cumulated vsize (Kb) 67248 [startup+850.087 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 84748 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 848.67 Current children cumulated vsize (Kb) 67248 [startup+860.087 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 85748 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134556712 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 858.67 Current children cumulated vsize (Kb) 67248 [startup+870.088 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 86748 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 868.67 Current children cumulated vsize (Kb) 67248 [startup+880.089 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 87748 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 878.67 Current children cumulated vsize (Kb) 67248 [startup+890.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 88749 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 888.68 Current children cumulated vsize (Kb) 67248 [startup+900.092 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16546 0 0 0 89749 117 0 0 25 0 1 0 1788279564 66686976 15859 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16281 15859 145 145 0 16136 0 [pid=24388] vsize: 65124 Current children cumulated CPU time (s) 898.68 Current children cumulated vsize (Kb) 67248 [startup+910.093 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 16924 0 0 0 90742 121 0 0 25 0 1 0 1788279564 68243456 16237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 16661 16237 145 145 0 16516 0 [pid=24388] vsize: 66644 Current children cumulated CPU time (s) 908.65 Current children cumulated vsize (Kb) 68768 [startup+920.092 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 17329 0 0 0 91736 123 0 0 25 0 1 0 1788279564 69910528 16642 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 17068 16642 145 145 0 16923 0 [pid=24388] vsize: 68272 Current children cumulated CPU time (s) 918.61 Current children cumulated vsize (Kb) 70396 [startup+930.093 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 17708 0 0 0 92731 125 0 0 25 0 1 0 1788279564 71467008 17021 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 17448 17021 145 145 0 17303 0 [pid=24388] vsize: 69792 Current children cumulated CPU time (s) 928.58 Current children cumulated vsize (Kb) 71916 [startup+940.094 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 18101 0 0 0 93724 127 0 0 25 0 1 0 1788279564 73076736 17414 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 17841 17414 145 145 0 17696 0 [pid=24388] vsize: 71364 Current children cumulated CPU time (s) 938.53 Current children cumulated vsize (Kb) 73488 [startup+950.095 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 18434 0 0 0 94717 130 0 0 25 0 1 0 1788279564 74444800 17747 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 18175 17747 145 145 0 18030 0 [pid=24388] vsize: 72700 Current children cumulated CPU time (s) 948.49 Current children cumulated vsize (Kb) 74824 [startup+960.096 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 18752 0 0 0 95712 133 0 0 25 0 1 0 1788279564 75763712 18065 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 18497 18065 145 145 0 18352 0 [pid=24388] vsize: 73988 Current children cumulated CPU time (s) 958.47 Current children cumulated vsize (Kb) 76112 [startup+970.097 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 19026 0 0 0 96706 135 0 0 25 0 1 0 1788279564 76886016 18339 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 18771 18339 145 145 0 18626 0 [pid=24388] vsize: 75084 Current children cumulated CPU time (s) 968.43 Current children cumulated vsize (Kb) 77208 [startup+980.097 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 19328 0 0 0 97701 137 0 0 25 0 1 0 1788279564 78151680 18641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24388/statm): 19080 18641 145 145 0 18935 0 [pid=24388] vsize: 76320 Current children cumulated CPU time (s) 978.4 Current children cumulated vsize (Kb) 78444 [startup+990.098 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 19535 0 0 0 98697 138 0 0 25 0 1 0 1788279564 78995456 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 19286 18848 145 145 0 19141 0 [pid=24388] vsize: 77144 Current children cumulated CPU time (s) 988.37 Current children cumulated vsize (Kb) 79268 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 19801 0 0 0 99694 140 0 0 25 0 1 0 1788279564 80080896 19114 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 19551 19114 145 145 0 19406 0 [pid=24388] vsize: 78204 Current children cumulated CPU time (s) 998.36 Current children cumulated vsize (Kb) 80328 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 20097 0 0 0 100688 142 0 0 25 0 1 0 1788279564 81293312 19410 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 19847 19410 145 145 0 19702 0 [pid=24388] vsize: 79388 Current children cumulated CPU time (s) 1008.32 Current children cumulated vsize (Kb) 81512 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 20414 0 0 0 101683 143 0 0 25 0 1 0 1788279564 82591744 19727 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 20164 19727 145 145 0 20019 0 [pid=24388] vsize: 80656 Current children cumulated CPU time (s) 1018.28 Current children cumulated vsize (Kb) 82780 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 20758 0 0 0 102676 146 0 0 25 0 1 0 1788279564 84000768 20071 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 20508 20071 145 145 0 20363 0 [pid=24388] vsize: 82032 Current children cumulated CPU time (s) 1028.24 Current children cumulated vsize (Kb) 84156 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 21146 0 0 0 103670 149 0 0 25 0 1 0 1788279564 85585920 20459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 20895 20459 145 145 0 20750 0 [pid=24388] vsize: 83580 Current children cumulated CPU time (s) 1038.21 Current children cumulated vsize (Kb) 85704 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 21485 0 0 0 104663 151 0 0 25 0 1 0 1788279564 86970368 20798 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 21233 20798 145 145 0 21088 0 [pid=24388] vsize: 84932 Current children cumulated CPU time (s) 1048.16 Current children cumulated vsize (Kb) 87056 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 21894 0 0 0 105657 153 0 0 25 0 1 0 1788279564 88637440 21207 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 21640 21207 145 145 0 21495 0 [pid=24388] vsize: 86560 Current children cumulated CPU time (s) 1058.12 Current children cumulated vsize (Kb) 88684 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 22263 0 0 0 106651 156 0 0 25 0 1 0 1788279564 90140672 21576 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 22007 21576 145 145 0 21862 0 [pid=24388] vsize: 88028 Current children cumulated CPU time (s) 1068.09 Current children cumulated vsize (Kb) 90152 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 22562 0 0 0 107647 158 0 0 25 0 1 0 1788279564 91885568 21875 4294967295 134512640 135094434 3221224432 3221223072 134562225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 22433 21875 145 145 0 22288 0 [pid=24388] vsize: 89732 Current children cumulated CPU time (s) 1078.07 Current children cumulated vsize (Kb) 91856 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 22863 0 0 0 108642 160 0 0 25 0 1 0 1788279564 93122560 22176 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 22735 22176 145 145 0 22590 0 [pid=24388] vsize: 90940 Current children cumulated CPU time (s) 1088.04 Current children cumulated vsize (Kb) 93064 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 23180 0 0 0 109636 162 0 0 25 0 1 0 1788279564 94420992 22493 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 23052 22493 145 145 0 22907 0 [pid=24388] vsize: 92208 Current children cumulated CPU time (s) 1098 Current children cumulated vsize (Kb) 94332 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 23482 0 0 0 110631 165 0 0 25 0 1 0 1788279564 95649792 22795 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 23352 22795 145 145 0 23207 0 [pid=24388] vsize: 93408 Current children cumulated CPU time (s) 1107.98 Current children cumulated vsize (Kb) 95532 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 23827 0 0 0 111624 167 0 0 25 0 1 0 1788279564 97062912 23140 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 23697 23140 145 145 0 23552 0 [pid=24388] vsize: 94788 Current children cumulated CPU time (s) 1117.93 Current children cumulated vsize (Kb) 96912 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24002 0 0 0 112622 168 0 0 25 0 1 0 1788279564 97775616 23315 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 23871 23315 145 145 0 23726 0 [pid=24388] vsize: 95484 Current children cumulated CPU time (s) 1127.92 Current children cumulated vsize (Kb) 97608 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24175 0 0 0 113619 170 0 0 25 0 1 0 1788279564 98492416 23488 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24046 23488 145 145 0 23901 0 [pid=24388] vsize: 96184 Current children cumulated CPU time (s) 1137.91 Current children cumulated vsize (Kb) 98308 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24354 0 0 0 114617 171 0 0 25 0 1 0 1788279564 99217408 23667 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24223 23667 145 145 0 24078 0 [pid=24388] vsize: 96892 Current children cumulated CPU time (s) 1147.9 Current children cumulated vsize (Kb) 99016 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24487 0 0 0 115615 172 0 0 25 0 1 0 1788279564 99753984 23800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24354 23800 145 145 0 24209 0 [pid=24388] vsize: 97416 Current children cumulated CPU time (s) 1157.89 Current children cumulated vsize (Kb) 99540 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24540 0 0 0 116615 172 0 0 25 0 1 0 1788279564 99966976 23853 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24406 23853 145 145 0 24261 0 [pid=24388] vsize: 97624 Current children cumulated CPU time (s) 1167.89 Current children cumulated vsize (Kb) 99748 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24540 0 0 0 117615 172 0 0 25 0 1 0 1788279564 99966976 23853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24406 23853 145 145 0 24261 0 [pid=24388] vsize: 97624 Current children cumulated CPU time (s) 1177.89 Current children cumulated vsize (Kb) 99748 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24540 0 0 0 118615 172 0 0 25 0 1 0 1788279564 99966976 23853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24406 23853 145 145 0 24261 0 [pid=24388] vsize: 97624 Current children cumulated CPU time (s) 1187.89 Current children cumulated vsize (Kb) 99748 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24540 0 0 0 119615 172 0 0 25 0 1 0 1788279564 99966976 23853 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24406 23853 145 145 0 24261 0 [pid=24388] vsize: 97624 Current children cumulated CPU time (s) 1197.89 Current children cumulated vsize (Kb) 99748 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24540 0 0 0 120616 172 0 0 25 0 1 0 1788279564 99966976 23853 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24406 23853 145 145 0 24261 0 [pid=24388] vsize: 97624 Current children cumulated CPU time (s) 1207.9 Current children cumulated vsize (Kb) 99748 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24388 Raw data (/proc/24384/stat): 24384 (minisat+_script) S 24383 24384 31915 0 -1 0 289 239 0 0 0 1 0 1 18 0 1 0 1788279559 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24384/statm): 531 226 485 147 0 384 0 [pid=24384] vsize: 2124 Raw data (/proc/24388/stat): 24388 (minisat+_64-bit) R 24384 24384 31915 0 -1 0 24540 0 0 0 120616 172 0 0 25 0 1 0 1788279564 99966976 23853 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24388/statm): 24406 23853 145 145 0 24261 0 [pid=24388] vsize: 97624 Current children cumulated CPU time (s) 1207.9 Current children cumulated vsize (Kb) 99748 Sending SIGTERM to -24384 Sleeping 2 seconds One traced child (pid=24384) ended because it received signal 15 (SIGTERM) One traced child (pid=24388) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.17 CPU time (s): 1207.93 CPU user time (s): 1206.16 CPU system time (s): 1.76873 CPU usage (%): 99.8151 Max. virtual memory (cumulated for all children) (Kb): 99748
ERROR: no interpretation found !