Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air01.opb |
MD5SUM | 90db1995bd949fc5ac74143a523f3bcf |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3398 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 771 |
Biggest coefficient in the objective function | 3698 |
Number of bits for the biggest coefficient in the objective function | 12 |
Sum of the numbers in the objective function | 1192753 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 3698 |
Number of bits of the biggest number in a constraint | 12 |
Biggest sum of numbers in a constraint | 1192753 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 112.221 |
Number of variables | 771 |
Total number of constraints | 794 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 794 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 438 |
LAUNCH ON wulflinc3 THE 2005-09-20 03:28:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3277 boxname=wulflinc3 idbench=933 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 90db1995bd949fc5ac74143a523f3bcf /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb IDLAUNCH: 3277 /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: 917612 kB Buffers: 12228 kB Cached: 78272 kB SwapCached: 824 kB Active: 22684 kB Inactive: 70452 kB HighTotal: 131008 kB HighFree: 48748 kB LowTotal: 903652 kB LowFree: 868864 kB SwapTotal: 2097136 kB SwapFree: 2095740 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5656 kB Slab: 18200 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:48:50 (client local time) WITH STATUS 10 IN 1207.57 SECONDS stats: 3277 7 1207.57 10
c Parsing PB file... c Converting 46 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####################### c -- Clauses(.)/Splits(s): (none) c ---[ 44]---> BDD-cost: 49 c ---[ 42]---> BDD-cost: 39 c ---[ 40]---> BDD-cost: 41 c ---[ 38]---> BDD-cost: 53 c ---[ 36]---> BDD-cost: 63 c ---[ 34]---> BDD-cost: 61 c ---[ 32]---> BDD-cost: 83 c ---[ 30]---> BDD-cost: 111 c ---[ 28]---> BDD-cost: 139 c ---[ 26]---> BDD-cost: 197 c ---[ 24]---> BDD-cost: 233 c ---[ 22]---> BDD-cost: 273 c ---[ 20]---> BDD-cost: 353 c ---[ 18]---> BDD-cost: 331 c ---[ 16]---> BDD-cost: 527 c ---[ 14]---> BDD-cost: 589 c ---[ 12]---> BDD-cost: 607 c ---[ 10]---> BDD-cost: 559 c ---[ 8]---> BDD-cost: 755 c ---[ 6]---> BDD-cost: 769 c ---[ 4]---> BDD-cost: 741 c ---[ 2]---> BDD-cost: 781 c ---[ 0]---> BDD-cost: 873 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 20564 53488 | 6854 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 9600[0m c ---[ 0]---> Adder-cost: 7920 maxlim: 1183153 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26 | 75865 251014 | 25288 26 1591 61.2 | 0.000 % | c ============================================================================== c [1mFound solution: 8437[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1184316 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43 | 75889 251167 | 25296 43 2039 47.4 | 0.000 % | c ============================================================================== c [1mFound solution: 8097[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1184656 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43 | 75893 251220 | 25297 43 2039 47.4 | 0.000 % | c ============================================================================== c [1mFound solution: 7212[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1185541 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43 | 75898 251280 | 25299 43 2039 47.4 | 0.000 % | c | 144 | 75898 251280 | 27828 144 12635 87.7 | 0.325 % | c | 299 | 75898 251280 | 30611 299 56525 189.0 | 0.325 % | c ============================================================================== c [1mFound solution: 7192[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1185561 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 380 | 75902 251328 | 25300 380 64997 171.0 | 0.325 % | c | 482 | 75902 251328 | 27830 482 73689 152.9 | 0.342 % | c ============================================================================== c [1mFound solution: 6795[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1185958 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 500 | 75913 251422 | 25304 500 75462 150.9 | 0.342 % | c | 602 | 75911 251416 | 27834 589 101508 172.3 | 0.383 % | c ============================================================================== c [1mFound solution: 6136[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1186617 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 627 | 75922 251503 | 25307 614 102021 166.2 | 0.383 % | c ============================================================================== c [1mFound solution: 5674[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1187079 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 636 | 75926 251538 | 25308 623 104929 168.4 | 0.383 % | c ============================================================================== c [1mFound solution: 5268[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1187485 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 707 | 75935 251625 | 25311 694 148809 214.4 | 0.383 % | c | 807 | 75935 251625 | 27842 794 164116 206.7 | 0.471 % | c | 959 | 75935 251625 | 30626 946 216548 228.9 | 0.471 % | c ============================================================================== c [1mFound solution: 4967[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1187786 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1024 | 75947 251722 | 25315 1011 227278 224.8 | 0.471 % | c | 1126 | 75849 251378 | 27846 1082 230798 213.3 | 0.618 % | c | 1276 | 75849 251378 | 30631 1232 255783 207.6 | 0.618 % | c | 1503 | 75849 251378 | 33694 1459 341321 233.9 | 0.618 % | c | 1843 | 75849 251378 | 37063 1799 484561 269.4 | 0.618 % | c | 2351 | 75849 251378 | 40770 2307 614206 266.2 | 0.618 % | c ============================================================================== c [1mFound solution: 4424[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1188329 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2373 | 75863 251475 | 25287 2329 622610 267.3 | 0.618 % | c | 2473 | 75863 251475 | 27815 2429 647783 266.7 | 0.659 % | c ============================================================================== c [1mFound solution: 4031[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1188722 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2502 | 75874 251568 | 25291 2458 651822 265.2 | 0.659 % | c | 2604 | 75874 251568 | 27820 2560 693972 271.1 | 0.700 % | c | 2758 | 75874 251568 | 30602 2714 760000 280.0 | 0.700 % | c | 2983 | 75858 251516 | 33662 2937 780081 265.6 | 0.717 % | c | 3320 | 75778 251253 | 37028 3270 839332 256.7 | 0.747 % | c | 3828 | 75778 251253 | 40731 3778 917899 243.0 | 0.747 % | c | 4588 | 75778 251253 | 44804 4538 1017540 224.2 | 0.747 % | c | 5740 | 75778 251253 | 49285 5690 1245667 218.9 | 0.747 % | c | 7450 | 75740 251123 | 54213 7391 1736031 234.9 | 0.752 % | c | 10012 | 75732 251093 | 59634 9950 2505022 251.8 | 0.788 % | c | 13858 | 75641 250272 | 65598 13790 3638851 263.9 | 0.805 % | c | 19627 | 75497 249754 | 72158 19517 5744723 294.3 | 0.946 % | c | 28277 | 75249 248858 | 79373 28087 8142276 289.9 | 1.193 % | c | 41260 | 74584 246540 | 87311 40517 12845986 317.1 | 1.834 % | c ============================================================================== c [1mFound solution: 4028[0m c ---[ 0]---> Adder-cost: 5870 maxlim: 1181265 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41313 | 115415 392358 | 38471 40551 12854302 317.0 | 1.834 % | c | 41413 | 115315 392026 | 42318 14973 4495990 300.3 | 1.573 % | c | 41564 | 115315 392026 | 46549 15124 4551965 301.0 | 1.573 % | c | 41792 | 115228 391725 | 51204 15339 4602004 300.0 | 1.643 % | c | 42129 | 115159 391482 | 56325 15665 4654142 297.1 | 1.695 % | c | 42635 | 115159 391482 | 61957 16171 4847597 299.8 | 1.695 % | c | 43394 | 115110 391319 | 68153 16923 5099834 301.4 | 1.735 % | c | 44533 | 115110 391319 | 74969 18062 5440269 301.2 | 1.735 % | c | 46242 | 114998 390919 | 82466 19703 5960565 302.5 | 1.813 % | c | 48809 | 114805 390274 | 90712 22236 6719946 302.2 | 1.962 % | c ============================================================================== c [1mFound solution: 3964[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1181329 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49554 | 114811 390324 | 38270 22981 6981447 303.8 | 1.962 % | c | 49654 | 114811 390324 | 42097 23081 6996626 303.1 | 1.975 % | c | 49807 | 114811 390324 | 46306 23234 7021554 302.2 | 1.975 % | c | 50034 | 114811 390324 | 50937 23461 7067586 301.2 | 1.975 % | c | 50371 | 114804 390301 | 56031 23796 7121915 299.3 | 1.979 % | c | 50881 | 114804 390301 | 61634 24306 7286853 299.8 | 1.979 % | c | 51640 | 114804 390301 | 67797 25065 7605785 303.4 | 1.979 % | c | 52779 | 114804 390301 | 74577 26204 7898848 301.4 | 1.979 % | c ============================================================================== c [1mFound solution: 3513[0m c ---[ 0]---> Adder-cost: 4434 maxlim: 1178082 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 52959 | 145575 500184 | 48525 26382 7970230 302.1 | 1.979 % | c | 53059 | 145575 500184 | 53377 26482 8010334 302.5 | 1.745 % | c | 53213 | 145575 500184 | 58715 26636 8062283 302.7 | 1.745 % | c | 53438 | 145575 500184 | 64586 26861 8163983 303.9 | 1.745 % | c | 53776 | 145575 500184 | 71045 27199 8322697 306.0 | 1.745 % | c | 54284 | 145575 500184 | 78149 27707 8492379 306.5 | 1.745 % | c | 55043 | 145575 500184 | 85964 28466 8839787 310.5 | 1.745 % | c | 56182 | 145559 500132 | 94561 29603 9240486 312.1 | 1.756 % | c | 57890 | 145559 500132 | 104017 31311 9754725 311.5 | 1.756 % | c | 60453 | 145559 500132 | 114419 33874 10762969 317.7 | 1.756 % | c | 64297 | 145444 499735 | 125861 37706 12206060 323.7 | 1.807 % | c | 70063 | 145444 499735 | 138447 43472 14511566 333.8 | 1.807 % | c | 78713 | 145428 499683 | 152292 52119 17507350 335.9 | 1.818 % | c | 91688 | 145301 499260 | 167521 65067 21564811 331.4 | 1.866 % | c c *** TERMINATED *** s SATISFIABLE v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 -CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 -CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 -CL000026_bit0 -CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 -CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 -CL000053_bit0 -CL000054_bit0 CL000055_bit0 -CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 CL000129_bit0 -CL000130_bit0 -CL000131_bit0 -CL000132_bit0 -CL000133_bit0 -CL000134_bit0 -CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 -CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 -CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 -CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 -CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 -CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 CL000513_bit0 -CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 -CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bit
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/4111/stat): 4111 (minisat+_script) R 4110 4111 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797059792 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/4111/statm): 174 3 169 147 0 27 0 [pid=4111] 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=4112 New process pid=4113 New process pid=4114 execve syscall for /bin/sed executable One traced child (pid=4113) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=4114) exited with status: 0 One traced child (pid=4112) exited with status: 0 New process pid=4115 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-13-7-air01.opb [startup+10.0033 s] Raw data (loadavg): 0.76 0.92 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 5591 0 0 0 959 19 0 0 25 0 1 0 1797059797 22994944 4601 4294967295 134512640 135094434 3221224448 3221222000 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5614 4601 145 145 0 5469 0 [pid=4115] vsize: 22456 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 24580 [startup+20.0052 s] Raw data (loadavg): 0.80 0.92 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 5907 0 0 0 1957 20 0 0 25 0 1 0 1797059797 23220224 4681 4294967295 134512640 135094434 3221224448 3221222164 134600159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5669 4681 145 145 0 5524 0 [pid=4115] vsize: 22676 Current children cumulated CPU time (s) 19.77 Current children cumulated vsize (Kb) 24800 [startup+30.006 s] Raw data (loadavg): 0.83 0.93 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 6113 0 0 0 2955 21 0 0 25 0 1 0 1797059797 23355392 4698 4294967295 134512640 135094434 3221224448 3221221952 134540740 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5702 4698 145 145 0 5557 0 [pid=4115] vsize: 22808 Current children cumulated CPU time (s) 29.76 Current children cumulated vsize (Kb) 24932 [startup+40.0069 s] Raw data (loadavg): 0.86 0.93 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 6409 0 0 0 3953 23 0 0 25 0 1 0 1797059797 23490560 4732 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5735 4732 145 145 0 5590 0 [pid=4115] vsize: 22940 Current children cumulated CPU time (s) 39.76 Current children cumulated vsize (Kb) 25064 [startup+50.0087 s] Raw data (loadavg): 0.88 0.93 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 6945 0 0 0 4949 25 0 0 25 0 1 0 1797059797 23777280 4770 4294967295 134512640 135094434 3221224448 3221221824 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5805 4770 145 145 0 5660 0 [pid=4115] vsize: 23220 Current children cumulated CPU time (s) 49.74 Current children cumulated vsize (Kb) 25344 [startup+60.0095 s] Raw data (loadavg): 0.90 0.93 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 7301 0 0 0 5945 27 0 0 25 0 1 0 1797059797 23797760 4775 4294967295 134512640 135094434 3221224448 3221221744 134677035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5810 4775 145 145 0 5665 0 [pid=4115] vsize: 23240 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 25364 [startup+70.0103 s] Raw data (loadavg): 0.91 0.93 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 7638 0 0 0 6943 28 0 0 25 0 1 0 1797059797 23977984 4820 4294967295 134512640 135094434 3221224448 3221222332 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5854 4820 145 145 0 5709 0 [pid=4115] vsize: 23416 Current children cumulated CPU time (s) 69.71 Current children cumulated vsize (Kb) 25540 [startup+80.0112 s] Raw data (loadavg): 0.92 0.93 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 8008 0 0 0 7940 30 0 0 25 0 1 0 1797059797 24309760 4901 4294967295 134512640 135094434 3221224448 3221222324 134676380 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 5935 4901 145 145 0 5790 0 [pid=4115] vsize: 23740 Current children cumulated CPU time (s) 79.7 Current children cumulated vsize (Kb) 25864 [startup+90.012 s] Raw data (loadavg): 0.94 0.94 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 8377 0 0 0 8936 32 0 0 25 0 1 0 1797059797 25694208 5236 4294967295 134512640 135094434 3221224448 3221223120 134556490 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 6273 5236 145 145 0 6128 0 [pid=4115] vsize: 25092 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 27216 [startup+100.013 s] Raw data (loadavg): 0.94 0.94 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9070 0 0 0 9931 35 0 0 25 0 1 0 1797059797 26116096 5340 4294967295 134512640 135094434 3221224448 3221222060 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 6376 5340 145 145 0 6231 0 [pid=4115] vsize: 25504 Current children cumulated CPU time (s) 99.66 Current children cumulated vsize (Kb) 27628 [startup+110.014 s] Raw data (loadavg): 0.95 0.94 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9232 0 0 0 10929 36 0 0 25 0 1 0 1797059797 26644480 5469 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 6505 5469 145 145 0 6360 0 [pid=4115] vsize: 26020 Current children cumulated CPU time (s) 109.65 Current children cumulated vsize (Kb) 28144 [startup+120.016 s] Raw data (loadavg): 0.96 0.94 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9497 0 0 0 11924 38 0 0 25 0 1 0 1797059797 27738112 5734 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 6772 5734 145 145 0 6627 0 [pid=4115] vsize: 27088 Current children cumulated CPU time (s) 119.62 Current children cumulated vsize (Kb) 29212 [startup+130.016 s] Raw data (loadavg): 0.97 0.94 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 9776 0 0 0 12918 41 0 0 25 0 1 0 1797059797 28876800 6013 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 7050 6013 145 145 0 6905 0 [pid=4115] vsize: 28200 Current children cumulated CPU time (s) 129.59 Current children cumulated vsize (Kb) 30324 [startup+140.018 s] Raw data (loadavg): 0.97 0.94 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 10142 0 0 0 13912 44 0 0 25 0 1 0 1797059797 30355456 6379 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 7411 6379 145 145 0 7266 0 [pid=4115] vsize: 29644 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 31768 [startup+150.02 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 10492 0 0 0 14907 46 0 0 25 0 1 0 1797059797 31813632 6729 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 7767 6729 145 145 0 7622 0 [pid=4115] vsize: 31068 Current children cumulated CPU time (s) 149.53 Current children cumulated vsize (Kb) 33192 [startup+160.02 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 10845 0 0 0 15901 48 0 0 25 0 1 0 1797059797 33255424 7082 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 8119 7082 145 145 0 7974 0 [pid=4115] vsize: 32476 Current children cumulated CPU time (s) 159.49 Current children cumulated vsize (Kb) 34600 [startup+170.021 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 11186 0 0 0 16897 50 0 0 25 0 1 0 1797059797 34648064 7423 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 8459 7423 145 145 0 8314 0 [pid=4115] vsize: 33836 Current children cumulated CPU time (s) 169.47 Current children cumulated vsize (Kb) 35960 [startup+180.022 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 11580 0 0 0 17889 53 0 0 25 0 1 0 1797059797 36257792 7817 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 8852 7817 145 145 0 8707 0 [pid=4115] vsize: 35408 Current children cumulated CPU time (s) 179.42 Current children cumulated vsize (Kb) 37532 [startup+190.023 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 11927 0 0 0 18882 56 0 0 25 0 1 0 1797059797 37675008 8164 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 9198 8164 145 145 0 9053 0 [pid=4115] vsize: 36792 Current children cumulated CPU time (s) 189.38 Current children cumulated vsize (Kb) 38916 [startup+200.024 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 12242 0 0 0 19877 59 0 0 25 0 1 0 1797059797 38961152 8479 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 9512 8479 145 145 0 9367 0 [pid=4115] vsize: 38048 Current children cumulated CPU time (s) 199.36 Current children cumulated vsize (Kb) 40172 [startup+210.025 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 12616 0 0 0 20873 60 0 0 25 0 1 0 1797059797 40484864 8853 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 9884 8853 145 145 0 9739 0 [pid=4115] vsize: 39536 Current children cumulated CPU time (s) 209.33 Current children cumulated vsize (Kb) 41660 [startup+220.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 12908 0 0 0 21869 63 0 0 25 0 1 0 1797059797 41680896 9145 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 10176 9145 145 145 0 10031 0 [pid=4115] vsize: 40704 Current children cumulated CPU time (s) 219.32 Current children cumulated vsize (Kb) 42828 [startup+230.027 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 13227 0 0 0 22865 65 0 0 25 0 1 0 1797059797 43048960 9464 4294967295 134512640 135094434 3221224448 3221223040 134556876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 10510 9464 145 145 0 10365 0 [pid=4115] vsize: 42040 Current children cumulated CPU time (s) 229.3 Current children cumulated vsize (Kb) 44164 [startup+240.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 13694 0 0 0 23857 68 0 0 25 0 1 0 1797059797 44961792 9931 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 10977 9931 145 145 0 10832 0 [pid=4115] vsize: 43908 Current children cumulated CPU time (s) 239.25 Current children cumulated vsize (Kb) 46032 [startup+250.028 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 14070 0 0 0 24852 71 0 0 25 0 1 0 1797059797 46493696 10307 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 11351 10307 145 145 0 11206 0 [pid=4115] vsize: 45404 Current children cumulated CPU time (s) 249.23 Current children cumulated vsize (Kb) 47528 [startup+260.028 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 14513 0 0 0 25846 74 0 0 25 0 1 0 1797059797 48304128 10750 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 11793 10750 145 145 0 11648 0 [pid=4115] vsize: 47172 Current children cumulated CPU time (s) 259.2 Current children cumulated vsize (Kb) 49296 [startup+270.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 14939 0 0 0 26841 76 0 0 25 0 1 0 1797059797 50049024 11176 4294967295 134512640 135094434 3221224448 3221223040 134556880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 12219 11176 145 145 0 12074 0 [pid=4115] vsize: 48876 Current children cumulated CPU time (s) 269.17 Current children cumulated vsize (Kb) 51000 [startup+280.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 15331 0 0 0 27835 78 0 0 25 0 1 0 1797059797 51646464 11568 4294967295 134512640 135094434 3221224448 3221223040 134557302 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 12609 11568 145 145 0 12464 0 [pid=4115] vsize: 50436 Current children cumulated CPU time (s) 279.13 Current children cumulated vsize (Kb) 52560 [startup+290.031 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 15479 0 0 0 28833 79 0 0 25 0 1 0 1797059797 52248576 11716 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 12756 11716 145 145 0 12611 0 [pid=4115] vsize: 51024 Current children cumulated CPU time (s) 289.12 Current children cumulated vsize (Kb) 53148 [startup+300.032 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 15842 0 0 0 29826 82 0 0 25 0 1 0 1797059797 53731328 12079 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 13118 12079 145 145 0 12973 0 [pid=4115] vsize: 52472 Current children cumulated CPU time (s) 299.08 Current children cumulated vsize (Kb) 54596 [startup+310.032 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 16178 0 0 0 30820 84 0 0 25 0 1 0 1797059797 55099392 12415 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 13452 12415 145 145 0 13307 0 [pid=4115] vsize: 53808 Current children cumulated CPU time (s) 309.04 Current children cumulated vsize (Kb) 55932 [startup+320.033 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 16450 0 0 0 31814 86 0 0 25 0 1 0 1797059797 56209408 12687 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 13723 12687 145 145 0 13578 0 [pid=4115] vsize: 54892 Current children cumulated CPU time (s) 319 Current children cumulated vsize (Kb) 57016 [startup+330.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 16756 0 0 0 32808 88 0 0 25 0 1 0 1797059797 57462784 12993 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 14029 12993 145 145 0 13884 0 [pid=4115] vsize: 56116 Current children cumulated CPU time (s) 328.96 Current children cumulated vsize (Kb) 58240 [startup+340.035 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) T 4111 4111 31915 0 -1 0 17001 0 0 0 33803 90 0 0 25 0 1 0 1797059797 58466304 13238 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4115/statm): 14274 13238 145 145 0 14129 0 [pid=4115] vsize: 57096 Current children cumulated CPU time (s) 338.93 Current children cumulated vsize (Kb) 59220 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 17309 0 0 0 34797 92 0 0 25 0 1 0 1797059797 59723776 13546 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 14581 13546 145 145 0 14436 0 [pid=4115] vsize: 58324 Current children cumulated CPU time (s) 348.89 Current children cumulated vsize (Kb) 60448 [startup+360.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 17686 0 0 0 35792 94 0 0 18 0 1 0 1797059797 61263872 13923 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 14957 13923 145 145 0 14812 0 [pid=4115] vsize: 59828 Current children cumulated CPU time (s) 358.86 Current children cumulated vsize (Kb) 61952 [startup+370.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18041 0 0 0 36786 96 0 0 25 0 1 0 1797059797 62713856 14278 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 15311 14278 145 145 0 15166 0 [pid=4115] vsize: 61244 Current children cumulated CPU time (s) 368.82 Current children cumulated vsize (Kb) 63368 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18250 0 0 0 37782 98 0 0 25 0 1 0 1797059797 63565824 14487 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 15519 14487 145 145 0 15374 0 [pid=4115] vsize: 62076 Current children cumulated CPU time (s) 378.8 Current children cumulated vsize (Kb) 64200 [startup+390.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18394 0 0 0 38780 99 0 0 25 0 1 0 1797059797 64163840 14631 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 15665 14631 145 145 0 15520 0 [pid=4115] vsize: 62660 Current children cumulated CPU time (s) 388.79 Current children cumulated vsize (Kb) 64784 [startup+400.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18682 0 0 0 39776 101 0 0 25 0 1 0 1797059797 65470464 14919 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 15984 14919 145 145 0 15839 0 [pid=4115] vsize: 63936 Current children cumulated CPU time (s) 398.77 Current children cumulated vsize (Kb) 66060 [startup+410.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 18992 0 0 0 40771 103 0 0 25 0 1 0 1797059797 66736128 15229 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 16293 15229 145 145 0 16148 0 [pid=4115] vsize: 65172 Current children cumulated CPU time (s) 408.74 Current children cumulated vsize (Kb) 67296 [startup+420.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 19332 0 0 0 41765 105 0 0 25 0 1 0 1797059797 68128768 15569 4294967295 134512640 135094434 3221224448 3221223040 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 16633 15569 145 145 0 16488 0 [pid=4115] vsize: 66532 Current children cumulated CPU time (s) 418.7 Current children cumulated vsize (Kb) 68656 [startup+430.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 19691 0 0 0 42758 108 0 0 25 0 1 0 1797059797 69599232 15928 4294967295 134512640 135094434 3221224448 3221223040 134556937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 16992 15928 145 145 0 16847 0 [pid=4115] vsize: 67968 Current children cumulated CPU time (s) 428.66 Current children cumulated vsize (Kb) 70092 [startup+440.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 20029 0 0 0 43753 110 0 0 25 0 1 0 1797059797 70979584 16266 4294967295 134512640 135094434 3221224448 3221223040 134556966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 17329 16266 145 145 0 17184 0 [pid=4115] vsize: 69316 Current children cumulated CPU time (s) 438.63 Current children cumulated vsize (Kb) 71440 [startup+450.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 20366 0 0 0 44749 112 0 0 25 0 1 0 1797059797 72355840 16603 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 17665 16603 145 145 0 17520 0 [pid=4115] vsize: 70660 Current children cumulated CPU time (s) 448.61 Current children cumulated vsize (Kb) 72784 [startup+460.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 20710 0 0 0 45742 115 0 0 25 0 1 0 1797059797 73764864 16947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 18009 16947 145 145 0 17864 0 [pid=4115] vsize: 72036 Current children cumulated CPU time (s) 458.57 Current children cumulated vsize (Kb) 74160 [startup+470.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 21059 0 0 0 46737 117 0 0 25 0 1 0 1797059797 75194368 17296 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 18358 17296 145 145 0 18213 0 [pid=4115] vsize: 73432 Current children cumulated CPU time (s) 468.54 Current children cumulated vsize (Kb) 75556 [startup+480.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 21457 0 0 0 47732 119 0 0 25 0 1 0 1797059797 76828672 17694 4294967295 134512640 135094434 3221224448 3221223136 134554707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 18757 17694 145 145 0 18612 0 [pid=4115] vsize: 75028 Current children cumulated CPU time (s) 478.51 Current children cumulated vsize (Kb) 77152 [startup+490.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 21814 0 0 0 48728 120 0 0 25 0 1 0 1797059797 78299136 18051 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19116 18051 145 145 0 18971 0 [pid=4115] vsize: 76464 Current children cumulated CPU time (s) 488.48 Current children cumulated vsize (Kb) 78588 [startup+500.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22608 0 0 0 49722 124 0 0 25 0 1 0 1797059797 79720448 18524 4294967295 134512640 135094434 3221224448 3221223236 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18524 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 498.46 Current children cumulated vsize (Kb) 79976 [startup+510.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 50721 124 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 508.45 Current children cumulated vsize (Kb) 79976 [startup+520.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 51721 124 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223120 134555566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 518.45 Current children cumulated vsize (Kb) 79976 [startup+530.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 52720 125 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 528.45 Current children cumulated vsize (Kb) 79976 [startup+540.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 53720 125 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223040 134556845 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 538.45 Current children cumulated vsize (Kb) 79976 [startup+550.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 54720 125 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 548.45 Current children cumulated vsize (Kb) 79976 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 55719 126 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 558.45 Current children cumulated vsize (Kb) 79976 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 56719 126 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223040 134556937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 568.45 Current children cumulated vsize (Kb) 79976 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 57718 126 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223040 134556987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 578.44 Current children cumulated vsize (Kb) 79976 [startup+590.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22614 0 0 0 58718 127 0 0 25 0 1 0 1797059797 79720448 18530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19463 18530 145 145 0 19318 0 [pid=4115] vsize: 77852 Current children cumulated CPU time (s) 588.45 Current children cumulated vsize (Kb) 79976 [startup+600.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 59716 128 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0 [pid=4115] vsize: 77996 Current children cumulated CPU time (s) 598.44 Current children cumulated vsize (Kb) 80120 [startup+610.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 60716 129 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0 [pid=4115] vsize: 77996 Current children cumulated CPU time (s) 608.45 Current children cumulated vsize (Kb) 80120 [startup+620.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 61715 129 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0 [pid=4115] vsize: 77996 Current children cumulated CPU time (s) 618.44 Current children cumulated vsize (Kb) 80120 [startup+630.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22774 0 0 0 62715 129 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221223040 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0 [pid=4115] vsize: 77996 Current children cumulated CPU time (s) 628.44 Current children cumulated vsize (Kb) 80120 [startup+640.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22899 0 0 0 63714 130 0 0 25 0 1 0 1797059797 79867904 18565 4294967295 134512640 135094434 3221224448 3221221280 134784948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19499 18565 145 145 0 19354 0 [pid=4115] vsize: 77996 Current children cumulated CPU time (s) 638.44 Current children cumulated vsize (Kb) 80120 [startup+650.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 64714 130 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 648.44 Current children cumulated vsize (Kb) 80632 [startup+660.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 65713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 658.44 Current children cumulated vsize (Kb) 80632 [startup+670.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 66713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 668.44 Current children cumulated vsize (Kb) 80632 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 67713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223040 134557025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 678.44 Current children cumulated vsize (Kb) 80632 [startup+690.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 68713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134558298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 688.44 Current children cumulated vsize (Kb) 80632 [startup+700.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 69713 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 698.44 Current children cumulated vsize (Kb) 80632 [startup+710.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 70714 131 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 708.45 Current children cumulated vsize (Kb) 80632 [startup+720.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 71713 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 718.45 Current children cumulated vsize (Kb) 80632 [startup+730.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 72714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 728.46 Current children cumulated vsize (Kb) 80632 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 73714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 738.46 Current children cumulated vsize (Kb) 80632 [startup+750.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 74714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 748.46 Current children cumulated vsize (Kb) 80632 [startup+760.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 75714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 758.46 Current children cumulated vsize (Kb) 80632 [startup+770.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 22997 0 0 0 76714 132 0 0 25 0 1 0 1797059797 80392192 18663 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19627 18663 145 145 0 19482 0 [pid=4115] vsize: 78508 Current children cumulated CPU time (s) 768.46 Current children cumulated vsize (Kb) 80632 [startup+780.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23029 0 0 0 77714 132 0 0 25 0 1 0 1797059797 80523264 18695 4294967295 134512640 135094434 3221224448 3221223072 134557683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19659 18695 145 145 0 19514 0 [pid=4115] vsize: 78636 Current children cumulated CPU time (s) 778.46 Current children cumulated vsize (Kb) 80760 [startup+790.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23304 0 0 0 78709 135 0 0 25 0 1 0 1797059797 81653760 18970 4294967295 134512640 135094434 3221224448 3221223040 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 19935 18970 145 145 0 19790 0 [pid=4115] vsize: 79740 Current children cumulated CPU time (s) 788.44 Current children cumulated vsize (Kb) 81864 [startup+800.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23601 0 0 0 79705 136 0 0 25 0 1 0 1797059797 82866176 19267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 20231 19267 145 145 0 20086 0 [pid=4115] vsize: 80924 Current children cumulated CPU time (s) 798.41 Current children cumulated vsize (Kb) 83048 [startup+810.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 23919 0 0 0 80700 138 0 0 25 0 1 0 1797059797 84168704 19585 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 20549 19585 145 145 0 20404 0 [pid=4115] vsize: 82196 Current children cumulated CPU time (s) 808.38 Current children cumulated vsize (Kb) 84320 [startup+820.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 24306 0 0 0 81695 140 0 0 25 0 1 0 1797059797 85753856 19972 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 20936 19972 145 145 0 20791 0 [pid=4115] vsize: 83744 Current children cumulated CPU time (s) 818.35 Current children cumulated vsize (Kb) 85868 [startup+830.083 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) T 4111 4111 31915 0 -1 0 24658 0 0 0 82690 142 0 0 25 0 1 0 1797059797 87195648 20324 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4115/statm): 21288 20324 145 145 0 21143 0 [pid=4115] vsize: 85152 Current children cumulated CPU time (s) 828.32 Current children cumulated vsize (Kb) 87276 [startup+840.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25013 0 0 0 83685 144 0 0 25 0 1 0 1797059797 88645632 20679 4294967295 134512640 135094434 3221224448 3221223120 134556505 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 21642 20679 145 145 0 21497 0 [pid=4115] vsize: 86568 Current children cumulated CPU time (s) 838.29 Current children cumulated vsize (Kb) 88692 [startup+850.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25338 0 0 0 84680 146 0 0 25 0 1 0 1797059797 89976832 21004 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 21967 21004 145 145 0 21822 0 [pid=4115] vsize: 87868 Current children cumulated CPU time (s) 848.26 Current children cumulated vsize (Kb) 89992 [startup+860.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25637 0 0 0 85675 149 0 0 25 0 1 0 1797059797 91197440 21303 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 22265 21303 145 145 0 22120 0 [pid=4115] vsize: 89060 Current children cumulated CPU time (s) 858.24 Current children cumulated vsize (Kb) 91184 [startup+870.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 25990 0 0 0 86670 151 0 0 25 0 1 0 1797059797 92639232 21656 4294967295 134512640 135094434 3221224448 3221223040 134557336 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 22617 21656 145 145 0 22472 0 [pid=4115] vsize: 90468 Current children cumulated CPU time (s) 868.21 Current children cumulated vsize (Kb) 92592 [startup+880.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 26218 0 0 0 87668 152 0 0 25 0 1 0 1797059797 93573120 21884 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 22845 21884 145 145 0 22700 0 [pid=4115] vsize: 91380 Current children cumulated CPU time (s) 878.2 Current children cumulated vsize (Kb) 93504 [startup+890.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 26525 0 0 0 88664 154 0 0 25 0 1 0 1797059797 94826496 22191 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 23151 22191 145 145 0 23006 0 [pid=4115] vsize: 92604 Current children cumulated CPU time (s) 888.18 Current children cumulated vsize (Kb) 94728 [startup+900.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 26839 0 0 0 89659 157 0 0 25 0 1 0 1797059797 96108544 22505 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 23464 22505 145 145 0 23319 0 [pid=4115] vsize: 93856 Current children cumulated CPU time (s) 898.16 Current children cumulated vsize (Kb) 95980 [startup+910.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27123 0 0 0 90654 159 0 0 25 0 1 0 1797059797 97271808 22789 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 23748 22789 145 145 0 23603 0 [pid=4115] vsize: 94992 Current children cumulated CPU time (s) 908.13 Current children cumulated vsize (Kb) 97116 [startup+920.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27460 0 0 0 91648 162 0 0 25 0 1 0 1797059797 98648064 23126 4294967295 134512640 135094434 3221224448 3221223040 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 24084 23126 145 145 0 23939 0 [pid=4115] vsize: 96336 Current children cumulated CPU time (s) 918.1 Current children cumulated vsize (Kb) 98460 [startup+930.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27735 0 0 0 92644 164 0 0 25 0 1 0 1797059797 99778560 23401 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 24360 23401 145 145 0 24215 0 [pid=4115] vsize: 97440 Current children cumulated CPU time (s) 928.08 Current children cumulated vsize (Kb) 99564 [startup+940.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 27932 0 0 0 93640 165 0 0 25 0 1 0 1797059797 100581376 23598 4294967295 134512640 135094434 3221224448 3221223040 134557210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 24556 23598 145 145 0 24411 0 [pid=4115] vsize: 98224 Current children cumulated CPU time (s) 938.05 Current children cumulated vsize (Kb) 100348 [startup+950.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28142 0 0 0 94637 167 0 0 25 0 1 0 1797059797 101441536 23808 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 24766 23808 145 145 0 24621 0 [pid=4115] vsize: 99064 Current children cumulated CPU time (s) 948.04 Current children cumulated vsize (Kb) 101188 [startup+960.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28343 0 0 0 95634 168 0 0 25 0 1 0 1797059797 102264832 24009 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 24967 24009 145 145 0 24822 0 [pid=4115] vsize: 99868 Current children cumulated CPU time (s) 958.02 Current children cumulated vsize (Kb) 101992 [startup+970.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28485 0 0 0 96632 169 0 0 25 0 1 0 1797059797 102842368 24151 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 25108 24151 145 145 0 24963 0 [pid=4115] vsize: 100432 Current children cumulated CPU time (s) 968.01 Current children cumulated vsize (Kb) 102556 [startup+980.097 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) T 4111 4111 31915 0 -1 0 28599 0 0 0 97630 170 0 0 25 0 1 0 1797059797 103309312 24265 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4115/statm): 25222 24265 145 145 0 25077 0 [pid=4115] vsize: 100888 Current children cumulated CPU time (s) 978 Current children cumulated vsize (Kb) 103012 [startup+990.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 28819 0 0 0 98627 171 0 0 25 0 1 0 1797059797 104206336 24485 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 25441 24485 145 145 0 25296 0 [pid=4115] vsize: 101764 Current children cumulated CPU time (s) 987.98 Current children cumulated vsize (Kb) 103888 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29014 0 0 0 99623 172 0 0 25 0 1 0 1797059797 105005056 24680 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 25636 24680 145 145 0 25491 0 [pid=4115] vsize: 102544 Current children cumulated CPU time (s) 997.95 Current children cumulated vsize (Kb) 104668 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29268 0 0 0 100619 174 0 0 25 0 1 0 1797059797 106045440 24934 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 25890 24934 145 145 0 25745 0 [pid=4115] vsize: 103560 Current children cumulated CPU time (s) 1007.93 Current children cumulated vsize (Kb) 105684 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29463 0 0 0 101617 175 0 0 25 0 1 0 1797059797 106840064 25129 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 26084 25129 145 145 0 25939 0 [pid=4115] vsize: 104336 Current children cumulated CPU time (s) 1017.92 Current children cumulated vsize (Kb) 106460 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29709 0 0 0 102613 177 0 0 25 0 1 0 1797059797 107851776 25375 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 26331 25375 145 145 0 26186 0 [pid=4115] vsize: 105324 Current children cumulated CPU time (s) 1027.9 Current children cumulated vsize (Kb) 107448 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 29889 0 0 0 103609 179 0 0 25 0 1 0 1797059797 108584960 25555 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 26510 25555 145 145 0 26365 0 [pid=4115] vsize: 106040 Current children cumulated CPU time (s) 1037.88 Current children cumulated vsize (Kb) 108164 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30100 0 0 0 104605 180 0 0 25 0 1 0 1797059797 109449216 25766 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 26721 25766 145 145 0 26576 0 [pid=4115] vsize: 106884 Current children cumulated CPU time (s) 1047.85 Current children cumulated vsize (Kb) 109008 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30278 0 0 0 105602 181 0 0 25 0 1 0 1797059797 110174208 25944 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 26898 25944 145 145 0 26753 0 [pid=4115] vsize: 107592 Current children cumulated CPU time (s) 1057.83 Current children cumulated vsize (Kb) 109716 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30502 0 0 0 106599 182 0 0 25 0 1 0 1797059797 111099904 26168 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 27124 26168 145 145 0 26979 0 [pid=4115] vsize: 108496 Current children cumulated CPU time (s) 1067.81 Current children cumulated vsize (Kb) 110620 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30752 0 0 0 107595 184 0 0 25 0 1 0 1797059797 112119808 26418 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 27373 26418 145 145 0 27228 0 [pid=4115] vsize: 109492 Current children cumulated CPU time (s) 1077.79 Current children cumulated vsize (Kb) 111616 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 30925 0 0 0 108592 186 0 0 25 0 1 0 1797059797 112828416 26591 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 27546 26591 145 145 0 27401 0 [pid=4115] vsize: 110184 Current children cumulated CPU time (s) 1087.78 Current children cumulated vsize (Kb) 112308 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31131 0 0 0 109589 186 0 0 25 0 1 0 1797059797 113672192 26797 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4115/statm): 27752 26797 145 145 0 27607 0 [pid=4115] vsize: 111008 Current children cumulated CPU time (s) 1097.75 Current children cumulated vsize (Kb) 113132 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31370 0 0 0 110584 188 0 0 25 0 1 0 1797059797 114642944 27036 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 27989 27036 145 145 0 27844 0 [pid=4115] vsize: 111956 Current children cumulated CPU time (s) 1107.72 Current children cumulated vsize (Kb) 114080 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31610 0 0 0 111579 190 0 0 25 0 1 0 1797059797 115617792 27276 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 28227 27276 145 145 0 28082 0 [pid=4115] vsize: 112908 Current children cumulated CPU time (s) 1117.69 Current children cumulated vsize (Kb) 115032 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 31816 0 0 0 112575 191 0 0 25 0 1 0 1797059797 116461568 27482 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 28433 27482 145 145 0 28288 0 [pid=4115] vsize: 113732 Current children cumulated CPU time (s) 1127.66 Current children cumulated vsize (Kb) 115856 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32026 0 0 0 113572 193 0 0 25 0 1 0 1797059797 117313536 27692 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 28641 27692 145 145 0 28496 0 [pid=4115] vsize: 114564 Current children cumulated CPU time (s) 1137.65 Current children cumulated vsize (Kb) 116688 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32279 0 0 0 114566 195 0 0 25 0 1 0 1797059797 118349824 27945 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 28894 27945 145 145 0 28749 0 [pid=4115] vsize: 115576 Current children cumulated CPU time (s) 1147.61 Current children cumulated vsize (Kb) 117700 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32466 0 0 0 115564 196 0 0 25 0 1 0 1797059797 119111680 28132 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 29080 28132 145 145 0 28935 0 [pid=4115] vsize: 116320 Current children cumulated CPU time (s) 1157.6 Current children cumulated vsize (Kb) 118444 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32568 0 0 0 116562 197 0 0 25 0 1 0 1797059797 119816192 28234 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 29252 28234 145 145 0 29107 0 [pid=4115] vsize: 117008 Current children cumulated CPU time (s) 1167.59 Current children cumulated vsize (Kb) 119132 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32745 0 0 0 117558 198 0 0 25 0 1 0 1797059797 120549376 28411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 29431 28411 145 145 0 29286 0 [pid=4115] vsize: 117724 Current children cumulated CPU time (s) 1177.56 Current children cumulated vsize (Kb) 119848 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 32957 0 0 0 118554 200 0 0 25 0 1 0 1797059797 121421824 28623 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 29644 28623 145 145 0 29499 0 [pid=4115] vsize: 118576 Current children cumulated CPU time (s) 1187.54 Current children cumulated vsize (Kb) 120700 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 33265 0 0 0 119549 203 0 0 25 0 1 0 1797059797 122679296 28931 4294967295 134512640 135094434 3221224448 3221223040 134556961 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 29951 28931 145 145 0 29806 0 [pid=4115] vsize: 119804 Current children cumulated CPU time (s) 1197.52 Current children cumulated vsize (Kb) 121928 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 33606 0 0 0 120546 205 0 0 25 0 1 0 1797059797 124080128 29272 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 30293 29272 145 145 0 30148 0 [pid=4115] vsize: 121172 Current children cumulated CPU time (s) 1207.51 Current children cumulated vsize (Kb) 123296 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4115 Raw data (/proc/4111/stat): 4111 (minisat+_script) S 4110 4111 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797059792 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/4111/statm): 531 226 485 147 0 384 0 [pid=4111] vsize: 2124 Raw data (/proc/4115/stat): 4115 (minisat+_64-bit) R 4111 4111 31915 0 -1 0 33606 0 0 0 120546 205 0 0 25 0 1 0 1797059797 124080128 29272 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4115/statm): 30293 29272 145 145 0 30148 0 [pid=4115] vsize: 121172 Current children cumulated CPU time (s) 1207.51 Current children cumulated vsize (Kb) 123296 Sending SIGTERM to -4111 Sleeping 2 seconds One traced child (pid=4111) ended because it received signal 15 (SIGTERM) One traced child (pid=4115) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.19 CPU time (s): 1207.57 CPU user time (s): 1205.46 CPU system time (s): 2.10668 CPU usage (%): 99.7838 Max. virtual memory (cumulated for all children) (Kb): 123296
ERROR: no interpretation found !