Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.215 |
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 wulflinc28 THE 2005-09-19 03:26:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2893 boxname=wulflinc28 idbench=549 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 90db1995bd949fc5ac74143a523f3bcf /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-air01.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-air01.opb IDLAUNCH: 2893 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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: 887404 kB Buffers: 35260 kB Cached: 83792 kB SwapCached: 696 kB Active: 72500 kB Inactive: 49112 kB HighTotal: 131008 kB HighFree: 43624 kB LowTotal: 903652 kB LowFree: 843780 kB SwapTotal: 2097640 kB SwapFree: 2096372 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5812 kB Slab: 20028 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:46:43 (client local time) WITH STATUS 10 IN 1207.62 SECONDS stats: 2893 7 1207.62 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/9152/stat): 9152 (minisat+_script) R 9151 9152 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846656055 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9152/statm): 174 3 169 147 0 27 0 [pid=9152] 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=9153 New process pid=9154 New process pid=9155 execve syscall for /bin/sed executable One traced child (pid=9154) 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=9155) exited with status: 0 One traced child (pid=9153) exited with status: 0 New process pid=9156 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-air01.opb [startup+10.0031 s] Raw data (loadavg): 1.01 0.97 0.95 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 5591 0 0 0 959 19 0 0 25 0 1 0 1846656060 22994944 4601 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5614 4601 145 145 0 5469 0 [pid=9156] vsize: 22456 Current children cumulated CPU time (s) 9.79 Current children cumulated vsize (Kb) 24580 [startup+20.0048 s] Raw data (loadavg): 1.08 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 5907 0 0 0 1958 20 0 0 25 0 1 0 1846656060 23220224 4681 4294967295 134512640 135094434 3221224432 3221221808 134676480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5669 4681 145 145 0 5524 0 [pid=9156] vsize: 22676 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 24800 [startup+30.0055 s] Raw data (loadavg): 1.07 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 6113 0 0 0 2956 21 0 0 25 0 1 0 1846656060 23355392 4698 4294967295 134512640 135094434 3221224432 3221221860 134541720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5702 4698 145 145 0 5557 0 [pid=9156] vsize: 22808 Current children cumulated CPU time (s) 29.78 Current children cumulated vsize (Kb) 24932 [startup+40.0062 s] Raw data (loadavg): 1.06 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 6409 0 0 0 3955 22 0 0 25 0 1 0 1846656060 23490560 4732 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5735 4732 145 145 0 5590 0 [pid=9156] vsize: 22940 Current children cumulated CPU time (s) 39.78 Current children cumulated vsize (Kb) 25064 [startup+50.0079 s] Raw data (loadavg): 1.05 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 6945 0 0 0 4949 25 0 0 25 0 1 0 1846656060 23777280 4770 4294967295 134512640 135094434 3221224432 3221222160 134600225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5805 4770 145 145 0 5660 0 [pid=9156] vsize: 23220 Current children cumulated CPU time (s) 49.75 Current children cumulated vsize (Kb) 25344 [startup+60.0076 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 7301 0 0 0 5946 27 0 0 25 0 1 0 1846656060 23797760 4775 4294967295 134512640 135094434 3221224432 3221221964 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5810 4775 145 145 0 5665 0 [pid=9156] vsize: 23240 Current children cumulated CPU time (s) 59.74 Current children cumulated vsize (Kb) 25364 [startup+70.0082 s] Raw data (loadavg): 1.03 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 7638 0 0 0 6943 28 0 0 25 0 1 0 1846656060 23977984 4820 4294967295 134512640 135094434 3221224432 3221222608 134676280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5854 4820 145 145 0 5709 0 [pid=9156] vsize: 23416 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 25540 [startup+80.0089 s] Raw data (loadavg): 1.03 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 8008 0 0 0 7940 30 0 0 25 0 1 0 1846656060 24309760 4901 4294967295 134512640 135094434 3221224432 3221222220 134676610 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 5935 4901 145 145 0 5790 0 [pid=9156] vsize: 23740 Current children cumulated CPU time (s) 79.71 Current children cumulated vsize (Kb) 25864 [startup+90.0096 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 8378 0 0 0 8935 32 0 0 25 0 1 0 1846656060 25698304 5237 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 6274 5237 145 145 0 6129 0 [pid=9156] vsize: 25096 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 27220 [startup+100.01 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9070 0 0 0 9929 36 0 0 25 0 1 0 1846656060 26116096 5340 4294967295 134512640 135094434 3221224432 3221221808 134601029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 6376 5340 145 145 0 6231 0 [pid=9156] vsize: 25504 Current children cumulated CPU time (s) 99.66 Current children cumulated vsize (Kb) 27628 [startup+110.011 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9232 0 0 0 10926 37 0 0 25 0 1 0 1846656060 26644480 5469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 6505 5469 145 145 0 6360 0 [pid=9156] vsize: 26020 Current children cumulated CPU time (s) 109.64 Current children cumulated vsize (Kb) 28144 [startup+120.012 s] Raw data (loadavg): 1.01 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9489 0 0 0 11921 40 0 0 25 0 1 0 1846656060 27705344 5726 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 6764 5726 145 145 0 6619 0 [pid=9156] vsize: 27056 Current children cumulated CPU time (s) 119.62 Current children cumulated vsize (Kb) 29180 [startup+130.012 s] Raw data (loadavg): 1.01 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 9767 0 0 0 12916 43 0 0 25 0 1 0 1846656060 28839936 6004 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 7041 6004 145 145 0 6896 0 [pid=9156] vsize: 28164 Current children cumulated CPU time (s) 129.6 Current children cumulated vsize (Kb) 30288 [startup+140.013 s] Raw data (loadavg): 1.01 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 10121 0 0 0 13910 45 0 0 25 0 1 0 1846656060 30273536 6358 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 7391 6358 145 145 0 7246 0 [pid=9156] vsize: 29564 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 31688 [startup+150.014 s] Raw data (loadavg): 1.01 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 10473 0 0 0 14905 47 0 0 25 0 1 0 1846656060 31739904 6710 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 7749 6710 145 145 0 7604 0 [pid=9156] vsize: 30996 Current children cumulated CPU time (s) 149.53 Current children cumulated vsize (Kb) 33120 [startup+160.013 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 10817 0 0 0 15899 49 0 0 25 0 1 0 1846656060 33140736 7054 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 8091 7054 145 145 0 7946 0 [pid=9156] vsize: 32364 Current children cumulated CPU time (s) 159.49 Current children cumulated vsize (Kb) 34488 [startup+170.014 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 11156 0 0 0 16894 51 0 0 25 0 1 0 1846656060 34525184 7393 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 8429 7393 145 145 0 8284 0 [pid=9156] vsize: 33716 Current children cumulated CPU time (s) 169.46 Current children cumulated vsize (Kb) 35840 [startup+180.014 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 11543 0 0 0 17886 55 0 0 25 0 1 0 1846656060 36106240 7780 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 8815 7780 145 145 0 8670 0 [pid=9156] vsize: 35260 Current children cumulated CPU time (s) 179.42 Current children cumulated vsize (Kb) 37384 [startup+190.014 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 11901 0 0 0 18880 58 0 0 25 0 1 0 1846656060 37568512 8138 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 9172 8138 145 145 0 9027 0 [pid=9156] vsize: 36688 Current children cumulated CPU time (s) 189.39 Current children cumulated vsize (Kb) 38812 [startup+200.015 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 12214 0 0 0 19874 60 0 0 25 0 1 0 1846656060 38846464 8451 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 9484 8451 145 145 0 9339 0 [pid=9156] vsize: 37936 Current children cumulated CPU time (s) 199.35 Current children cumulated vsize (Kb) 40060 [startup+210.015 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 12592 0 0 0 20867 63 0 0 25 0 1 0 1846656060 40386560 8829 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 9860 8829 145 145 0 9715 0 [pid=9156] vsize: 39440 Current children cumulated CPU time (s) 209.31 Current children cumulated vsize (Kb) 41564 [startup+220.016 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 12869 0 0 0 21862 66 0 0 25 0 1 0 1846656060 41521152 9106 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 10137 9106 145 145 0 9992 0 [pid=9156] vsize: 40548 Current children cumulated CPU time (s) 219.29 Current children cumulated vsize (Kb) 42672 [startup+230.016 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 13199 0 0 0 22858 68 0 0 25 0 1 0 1846656060 42934272 9436 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 10482 9436 145 145 0 10337 0 [pid=9156] vsize: 41928 Current children cumulated CPU time (s) 229.27 Current children cumulated vsize (Kb) 44052 [startup+240.017 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 13658 0 0 0 23851 71 0 0 25 0 1 0 1846656060 44810240 9895 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 10940 9895 145 145 0 10795 0 [pid=9156] vsize: 43760 Current children cumulated CPU time (s) 239.23 Current children cumulated vsize (Kb) 45884 [startup+250.018 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 14038 0 0 0 24847 73 0 0 25 0 1 0 1846656060 46362624 10275 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 11319 10275 145 145 0 11174 0 [pid=9156] vsize: 45276 Current children cumulated CPU time (s) 249.21 Current children cumulated vsize (Kb) 47400 [startup+260.018 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 14472 0 0 0 25840 75 0 0 25 0 1 0 1846656060 48144384 10709 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 11754 10709 145 145 0 11609 0 [pid=9156] vsize: 47016 Current children cumulated CPU time (s) 259.16 Current children cumulated vsize (Kb) 49140 [startup+270.019 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 14905 0 0 0 26835 78 0 0 25 0 1 0 1846656060 49905664 11142 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 12184 11142 145 145 0 12039 0 [pid=9156] vsize: 48736 Current children cumulated CPU time (s) 269.14 Current children cumulated vsize (Kb) 50860 [startup+280.02 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 15308 0 0 0 27829 80 0 0 25 0 1 0 1846656060 51552256 11545 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 12586 11545 145 145 0 12441 0 [pid=9156] vsize: 50344 Current children cumulated CPU time (s) 279.1 Current children cumulated vsize (Kb) 52468 [startup+290.021 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 15463 0 0 0 28828 81 0 0 25 0 1 0 1846656060 52183040 11700 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 12740 11700 145 145 0 12595 0 [pid=9156] vsize: 50960 Current children cumulated CPU time (s) 289.1 Current children cumulated vsize (Kb) 53084 [startup+300.022 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 15811 0 0 0 29822 84 0 0 25 0 1 0 1846656060 53604352 12048 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 13087 12048 145 145 0 12942 0 [pid=9156] vsize: 52348 Current children cumulated CPU time (s) 299.07 Current children cumulated vsize (Kb) 54472 [startup+310.022 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16148 0 0 0 30814 87 0 0 25 0 1 0 1846656060 54980608 12385 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 13423 12385 145 145 0 13278 0 [pid=9156] vsize: 53692 Current children cumulated CPU time (s) 309.02 Current children cumulated vsize (Kb) 55816 [startup+320.022 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16435 0 0 0 31808 89 0 0 25 0 1 0 1846656060 56147968 12672 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 13708 12672 145 145 0 13563 0 [pid=9156] vsize: 54832 Current children cumulated CPU time (s) 318.98 Current children cumulated vsize (Kb) 56956 [startup+330.023 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16733 0 0 0 32803 92 0 0 25 0 1 0 1846656060 57368576 12970 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 14006 12970 145 145 0 13861 0 [pid=9156] vsize: 56024 Current children cumulated CPU time (s) 328.96 Current children cumulated vsize (Kb) 58148 [startup+340.024 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 16991 0 0 0 33798 94 0 0 25 0 1 0 1846656060 58425344 13228 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 14264 13228 145 145 0 14119 0 [pid=9156] vsize: 57056 Current children cumulated CPU time (s) 338.93 Current children cumulated vsize (Kb) 59180 [startup+350.024 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 17300 0 0 0 34793 96 0 0 25 0 1 0 1846656060 59686912 13537 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 14572 13537 145 145 0 14427 0 [pid=9156] vsize: 58288 Current children cumulated CPU time (s) 348.9 Current children cumulated vsize (Kb) 60412 [startup+360.025 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 17674 0 0 0 35787 99 0 0 25 0 1 0 1846656060 61214720 13911 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 14945 13911 145 145 0 14800 0 [pid=9156] vsize: 59780 Current children cumulated CPU time (s) 358.87 Current children cumulated vsize (Kb) 61904 [startup+370.026 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18038 0 0 0 36782 101 0 0 25 0 1 0 1846656060 62701568 14275 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 15308 14275 145 145 0 15163 0 [pid=9156] vsize: 61232 Current children cumulated CPU time (s) 368.84 Current children cumulated vsize (Kb) 63356 [startup+380.027 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18241 0 0 0 37779 103 0 0 25 0 1 0 1846656060 63528960 14478 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 15510 14478 145 145 0 15365 0 [pid=9156] vsize: 62040 Current children cumulated CPU time (s) 378.83 Current children cumulated vsize (Kb) 64164 [startup+390.028 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18394 0 0 0 38777 103 0 0 25 0 1 0 1846656060 64163840 14631 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 15665 14631 145 145 0 15520 0 [pid=9156] vsize: 62660 Current children cumulated CPU time (s) 388.81 Current children cumulated vsize (Kb) 64784 [startup+400.029 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18675 0 0 0 39772 105 0 0 25 0 1 0 1846656060 65441792 14912 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 15977 14912 145 145 0 15832 0 [pid=9156] vsize: 63908 Current children cumulated CPU time (s) 398.78 Current children cumulated vsize (Kb) 66032 [startup+410.03 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 18985 0 0 0 40767 107 0 0 25 0 1 0 1846656060 66707456 15222 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 16286 15222 145 145 0 16141 0 [pid=9156] vsize: 65144 Current children cumulated CPU time (s) 408.75 Current children cumulated vsize (Kb) 67268 [startup+420.03 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 19327 0 0 0 41761 110 0 0 25 0 1 0 1846656060 68108288 15564 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 16628 15564 145 145 0 16483 0 [pid=9156] vsize: 66512 Current children cumulated CPU time (s) 418.72 Current children cumulated vsize (Kb) 68636 [startup+430.031 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 19684 0 0 0 42755 112 0 0 25 0 1 0 1846656060 69570560 15921 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 16985 15921 145 145 0 16840 0 [pid=9156] vsize: 67940 Current children cumulated CPU time (s) 428.68 Current children cumulated vsize (Kb) 70064 [startup+440.032 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 20024 0 0 0 43749 115 0 0 25 0 1 0 1846656060 70959104 16261 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 17324 16261 145 145 0 17179 0 [pid=9156] vsize: 69296 Current children cumulated CPU time (s) 438.65 Current children cumulated vsize (Kb) 71420 [startup+450.032 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 20364 0 0 0 44745 117 0 0 25 0 1 0 1846656060 72347648 16601 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 17663 16601 145 145 0 17518 0 [pid=9156] vsize: 70652 Current children cumulated CPU time (s) 448.63 Current children cumulated vsize (Kb) 72776 [startup+460.033 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 20706 0 0 0 45740 119 0 0 25 0 1 0 1846656060 73748480 16943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 18005 16943 145 145 0 17860 0 [pid=9156] vsize: 72020 Current children cumulated CPU time (s) 458.6 Current children cumulated vsize (Kb) 74144 [startup+470.035 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 21057 0 0 0 46735 122 0 0 25 0 1 0 1846656060 75186176 17294 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 18356 17294 145 145 0 18211 0 [pid=9156] vsize: 73424 Current children cumulated CPU time (s) 468.58 Current children cumulated vsize (Kb) 75548 [startup+480.035 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 21456 0 0 0 47729 124 0 0 25 0 1 0 1846656060 76824576 17693 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 18756 17693 145 145 0 18611 0 [pid=9156] vsize: 75024 Current children cumulated CPU time (s) 478.54 Current children cumulated vsize (Kb) 77148 [startup+490.036 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 21814 0 0 0 48725 126 0 0 25 0 1 0 1846656060 78299136 18051 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19116 18051 145 145 0 18971 0 [pid=9156] vsize: 76464 Current children cumulated CPU time (s) 488.52 Current children cumulated vsize (Kb) 78588 [startup+500.038 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22608 0 0 0 49718 129 0 0 25 0 1 0 1846656060 79720448 18524 4294967295 134512640 135094434 3221224432 3221223248 134558992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18524 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 498.48 Current children cumulated vsize (Kb) 79976 [startup+510.038 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 50717 130 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 508.48 Current children cumulated vsize (Kb) 79976 [startup+520.039 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 51717 130 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 518.48 Current children cumulated vsize (Kb) 79976 [startup+530.04 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 52716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223104 134555556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 528.48 Current children cumulated vsize (Kb) 79976 [startup+540.04 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 53716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 538.48 Current children cumulated vsize (Kb) 79976 [startup+550.041 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 54716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 548.48 Current children cumulated vsize (Kb) 79976 [startup+560.042 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 55716 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 558.48 Current children cumulated vsize (Kb) 79976 [startup+570.044 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 56715 131 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 568.47 Current children cumulated vsize (Kb) 79976 [startup+580.044 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 57715 132 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 578.48 Current children cumulated vsize (Kb) 79976 [startup+590.046 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22614 0 0 0 58715 132 0 0 25 0 1 0 1846656060 79720448 18530 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19463 18530 145 145 0 19318 0 [pid=9156] vsize: 77852 Current children cumulated CPU time (s) 588.48 Current children cumulated vsize (Kb) 79976 [startup+600.048 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 59714 133 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0 [pid=9156] vsize: 77996 Current children cumulated CPU time (s) 598.48 Current children cumulated vsize (Kb) 80120 [startup+610.048 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 60713 133 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0 [pid=9156] vsize: 77996 Current children cumulated CPU time (s) 608.47 Current children cumulated vsize (Kb) 80120 [startup+620.05 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 61713 134 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0 [pid=9156] vsize: 77996 Current children cumulated CPU time (s) 618.48 Current children cumulated vsize (Kb) 80120 [startup+630.051 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22774 0 0 0 62712 134 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0 [pid=9156] vsize: 77996 Current children cumulated CPU time (s) 628.47 Current children cumulated vsize (Kb) 80120 [startup+640.051 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22899 0 0 0 63712 135 0 0 25 0 1 0 1846656060 79867904 18565 4294967295 134512640 135094434 3221224432 3221221360 134541721 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19499 18565 145 145 0 19354 0 [pid=9156] vsize: 77996 Current children cumulated CPU time (s) 638.48 Current children cumulated vsize (Kb) 80120 [startup+650.052 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 64711 135 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 648.47 Current children cumulated vsize (Kb) 80632 [startup+660.053 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 65711 135 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 658.47 Current children cumulated vsize (Kb) 80632 [startup+670.054 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 66711 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 668.48 Current children cumulated vsize (Kb) 80632 [startup+680.055 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 67711 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 678.48 Current children cumulated vsize (Kb) 80632 [startup+690.057 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 68710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 688.47 Current children cumulated vsize (Kb) 80632 [startup+700.058 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 69710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 698.47 Current children cumulated vsize (Kb) 80632 [startup+710.058 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 70710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 708.47 Current children cumulated vsize (Kb) 80632 [startup+720.06 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 71710 136 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 718.47 Current children cumulated vsize (Kb) 80632 [startup+730.061 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 72709 137 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 728.47 Current children cumulated vsize (Kb) 80632 [startup+740.062 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 73709 137 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 738.47 Current children cumulated vsize (Kb) 80632 [startup+750.063 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 74709 138 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 748.48 Current children cumulated vsize (Kb) 80632 [startup+760.063 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 75709 138 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 758.48 Current children cumulated vsize (Kb) 80632 [startup+770.064 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 22997 0 0 0 76709 138 0 0 25 0 1 0 1846656060 80392192 18663 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19627 18663 145 145 0 19482 0 [pid=9156] vsize: 78508 Current children cumulated CPU time (s) 768.48 Current children cumulated vsize (Kb) 80632 [startup+780.065 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23050 0 0 0 77709 138 0 0 25 0 1 0 1846656060 80609280 18716 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19680 18716 145 145 0 19535 0 [pid=9156] vsize: 78720 Current children cumulated CPU time (s) 778.48 Current children cumulated vsize (Kb) 80844 [startup+790.066 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23322 0 0 0 78705 140 0 0 25 0 1 0 1846656060 81723392 18988 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 19952 18988 145 145 0 19807 0 [pid=9156] vsize: 79808 Current children cumulated CPU time (s) 788.46 Current children cumulated vsize (Kb) 81932 [startup+800.066 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23623 0 0 0 79699 142 0 0 25 0 1 0 1846656060 82956288 19289 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 20253 19289 145 145 0 20108 0 [pid=9156] vsize: 81012 Current children cumulated CPU time (s) 798.42 Current children cumulated vsize (Kb) 83136 [startup+810.067 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 23948 0 0 0 80694 145 0 0 25 0 1 0 1846656060 84287488 19614 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 20578 19614 145 145 0 20433 0 [pid=9156] vsize: 82312 Current children cumulated CPU time (s) 808.4 Current children cumulated vsize (Kb) 84436 [startup+820.068 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 24332 0 0 0 81689 147 0 0 25 0 1 0 1846656060 85856256 19998 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 20961 19998 145 145 0 20816 0 [pid=9156] vsize: 83844 Current children cumulated CPU time (s) 818.37 Current children cumulated vsize (Kb) 85968 [startup+830.068 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 24684 0 0 0 82684 149 0 0 25 0 1 0 1846656060 87298048 20350 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 21313 20350 145 145 0 21168 0 [pid=9156] vsize: 85252 Current children cumulated CPU time (s) 828.34 Current children cumulated vsize (Kb) 87376 [startup+840.069 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 25037 0 0 0 83679 151 0 0 25 0 1 0 1846656060 88748032 20703 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 21667 20703 145 145 0 21522 0 [pid=9156] vsize: 86668 Current children cumulated CPU time (s) 838.31 Current children cumulated vsize (Kb) 88792 [startup+850.07 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 25360 0 0 0 84674 153 0 0 25 0 1 0 1846656060 90066944 21026 4294967295 134512640 135094434 3221224432 3221223024 134556891 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 21989 21026 145 145 0 21844 0 [pid=9156] vsize: 87956 Current children cumulated CPU time (s) 848.28 Current children cumulated vsize (Kb) 90080 [startup+860.071 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 25671 0 0 0 85669 155 0 0 25 0 1 0 1846656060 91336704 21337 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 22299 21337 145 145 0 22154 0 [pid=9156] vsize: 89196 Current children cumulated CPU time (s) 858.25 Current children cumulated vsize (Kb) 91320 [startup+870.072 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26001 0 0 0 86664 157 0 0 25 0 1 0 1846656060 92684288 21667 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 22628 21667 145 145 0 22483 0 [pid=9156] vsize: 90512 Current children cumulated CPU time (s) 868.22 Current children cumulated vsize (Kb) 92636 [startup+880.073 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26245 0 0 0 87659 159 0 0 25 0 1 0 1846656060 93683712 21911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 22872 21911 145 145 0 22727 0 [pid=9156] vsize: 91488 Current children cumulated CPU time (s) 878.19 Current children cumulated vsize (Kb) 93612 [startup+890.074 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26546 0 0 0 88655 161 0 0 25 0 1 0 1846656060 94912512 22212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 23172 22212 145 145 0 23027 0 [pid=9156] vsize: 92688 Current children cumulated CPU time (s) 888.17 Current children cumulated vsize (Kb) 94812 [startup+900.074 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 26872 0 0 0 89649 163 0 0 25 0 1 0 1846656060 96243712 22538 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 23497 22538 145 145 0 23352 0 [pid=9156] vsize: 93988 Current children cumulated CPU time (s) 898.13 Current children cumulated vsize (Kb) 96112 [startup+910.074 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27154 0 0 0 90646 164 0 0 25 0 1 0 1846656060 97398784 22820 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 23779 22820 145 145 0 23634 0 [pid=9156] vsize: 95116 Current children cumulated CPU time (s) 908.11 Current children cumulated vsize (Kb) 97240 [startup+920.075 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27492 0 0 0 91640 166 0 0 25 0 1 0 1846656060 98779136 23158 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 24116 23158 145 145 0 23971 0 [pid=9156] vsize: 96464 Current children cumulated CPU time (s) 918.07 Current children cumulated vsize (Kb) 98588 [startup+930.075 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27753 0 0 0 92637 168 0 0 25 0 1 0 1846656060 99852288 23419 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 24378 23419 145 145 0 24233 0 [pid=9156] vsize: 97512 Current children cumulated CPU time (s) 928.06 Current children cumulated vsize (Kb) 99636 [startup+940.076 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 27963 0 0 0 93633 169 0 0 25 0 1 0 1846656060 100708352 23629 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 24587 23629 145 145 0 24442 0 [pid=9156] vsize: 98348 Current children cumulated CPU time (s) 938.03 Current children cumulated vsize (Kb) 100472 [startup+950.077 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28173 0 0 0 94630 171 0 0 25 0 1 0 1846656060 101568512 23839 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 24797 23839 145 145 0 24652 0 [pid=9156] vsize: 99188 Current children cumulated CPU time (s) 948.02 Current children cumulated vsize (Kb) 101312 [startup+960.076 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28361 0 0 0 95628 172 0 0 25 0 1 0 1846656060 102338560 24027 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 24985 24027 145 145 0 24840 0 [pid=9156] vsize: 99940 Current children cumulated CPU time (s) 958.01 Current children cumulated vsize (Kb) 102064 [startup+970.077 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28485 0 0 0 96627 173 0 0 25 0 1 0 1846656060 102842368 24151 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 25108 24151 145 145 0 24963 0 [pid=9156] vsize: 100432 Current children cumulated CPU time (s) 968.01 Current children cumulated vsize (Kb) 102556 [startup+980.078 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28625 0 0 0 97624 173 0 0 25 0 1 0 1846656060 103415808 24291 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 25248 24291 145 145 0 25103 0 [pid=9156] vsize: 100992 Current children cumulated CPU time (s) 977.98 Current children cumulated vsize (Kb) 103116 [startup+990.078 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 28846 0 0 0 98621 175 0 0 25 0 1 0 1846656060 104321024 24512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 25469 24512 145 145 0 25324 0 [pid=9156] vsize: 101876 Current children cumulated CPU time (s) 987.97 Current children cumulated vsize (Kb) 104000 [startup+1000.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29042 0 0 0 99617 176 0 0 25 0 1 0 1846656060 105119744 24708 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 25664 24708 145 145 0 25519 0 [pid=9156] vsize: 102656 Current children cumulated CPU time (s) 997.94 Current children cumulated vsize (Kb) 104780 [startup+1010.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29294 0 0 0 100612 178 0 0 25 0 1 0 1846656060 106151936 24960 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 25916 24960 145 145 0 25771 0 [pid=9156] vsize: 103664 Current children cumulated CPU time (s) 1007.91 Current children cumulated vsize (Kb) 105788 [startup+1020.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29484 0 0 0 101609 179 0 0 25 0 1 0 1846656060 106926080 25150 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 26105 25150 145 145 0 25960 0 [pid=9156] vsize: 104420 Current children cumulated CPU time (s) 1017.89 Current children cumulated vsize (Kb) 106544 [startup+1030.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29734 0 0 0 102606 180 0 0 25 0 1 0 1846656060 107954176 25400 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 26356 25400 145 145 0 26211 0 [pid=9156] vsize: 105424 Current children cumulated CPU time (s) 1027.87 Current children cumulated vsize (Kb) 107548 [startup+1040.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 29910 0 0 0 103604 181 0 0 25 0 1 0 1846656060 108670976 25576 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 26531 25576 145 145 0 26386 0 [pid=9156] vsize: 106124 Current children cumulated CPU time (s) 1037.86 Current children cumulated vsize (Kb) 108248 [startup+1050.08 s] Raw data (loadavg): 1.00 0.99 0.96 3/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30120 0 0 0 104601 182 0 0 25 0 1 0 1846656060 109531136 25786 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 26741 25786 145 145 0 26596 0 [pid=9156] vsize: 106964 Current children cumulated CPU time (s) 1047.84 Current children cumulated vsize (Kb) 109088 [startup+1060.08 s] Raw data (loadavg): 1.00 0.99 0.96 1/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) T 9152 9152 20115 0 -1 0 30302 0 0 0 105597 183 0 0 25 0 1 0 1846656060 110272512 25968 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9156/statm): 26922 25968 145 145 0 26777 0 [pid=9156] vsize: 107688 Current children cumulated CPU time (s) 1057.81 Current children cumulated vsize (Kb) 109812 [startup+1070.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30532 0 0 0 106593 186 0 0 25 0 1 0 1846656060 111218688 26198 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 27153 26198 145 145 0 27008 0 [pid=9156] vsize: 108612 Current children cumulated CPU time (s) 1067.8 Current children cumulated vsize (Kb) 110736 [startup+1080.08 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30774 0 0 0 107590 187 0 0 25 0 1 0 1846656060 112209920 26440 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 27395 26440 145 145 0 27250 0 [pid=9156] vsize: 109580 Current children cumulated CPU time (s) 1077.78 Current children cumulated vsize (Kb) 111704 [startup+1090.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 30945 0 0 0 108588 188 0 0 25 0 1 0 1846656060 112910336 26611 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 27566 26611 145 145 0 27421 0 [pid=9156] vsize: 110264 Current children cumulated CPU time (s) 1087.77 Current children cumulated vsize (Kb) 112388 [startup+1100.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31161 0 0 0 109585 190 0 0 25 0 1 0 1846656060 113795072 26827 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 27782 26827 145 145 0 27637 0 [pid=9156] vsize: 111128 Current children cumulated CPU time (s) 1097.76 Current children cumulated vsize (Kb) 113252 [startup+1110.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31401 0 0 0 110582 191 0 0 25 0 1 0 1846656060 114769920 27067 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 28020 27067 145 145 0 27875 0 [pid=9156] vsize: 112080 Current children cumulated CPU time (s) 1107.74 Current children cumulated vsize (Kb) 114204 [startup+1120.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31635 0 0 0 111578 193 0 0 25 0 1 0 1846656060 115720192 27301 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 28252 27301 145 145 0 28107 0 [pid=9156] vsize: 113008 Current children cumulated CPU time (s) 1117.72 Current children cumulated vsize (Kb) 115132 [startup+1130.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 31835 0 0 0 112574 195 0 0 25 0 1 0 1846656060 116539392 27501 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 28452 27501 145 145 0 28307 0 [pid=9156] vsize: 113808 Current children cumulated CPU time (s) 1127.7 Current children cumulated vsize (Kb) 115932 [startup+1140.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32047 0 0 0 113571 196 0 0 25 0 1 0 1846656060 117399552 27713 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 28662 27713 145 145 0 28517 0 [pid=9156] vsize: 114648 Current children cumulated CPU time (s) 1137.68 Current children cumulated vsize (Kb) 116772 [startup+1150.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32294 0 0 0 114568 197 0 0 25 0 1 0 1846656060 118411264 27960 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 28909 27960 145 145 0 28764 0 [pid=9156] vsize: 115636 Current children cumulated CPU time (s) 1147.66 Current children cumulated vsize (Kb) 117760 [startup+1160.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32479 0 0 0 115565 198 0 0 25 0 1 0 1846656060 119164928 28145 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9156/statm): 29093 28145 145 145 0 28948 0 [pid=9156] vsize: 116372 Current children cumulated CPU time (s) 1157.64 Current children cumulated vsize (Kb) 118496 [startup+1170.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32579 0 0 0 116564 199 0 0 25 0 1 0 1846656060 119865344 28245 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 29264 28245 145 145 0 29119 0 [pid=9156] vsize: 117056 Current children cumulated CPU time (s) 1167.64 Current children cumulated vsize (Kb) 119180 [startup+1180.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32759 0 0 0 117562 200 0 0 25 0 1 0 1846656060 120606720 28425 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 29445 28425 145 145 0 29300 0 [pid=9156] vsize: 117780 Current children cumulated CPU time (s) 1177.63 Current children cumulated vsize (Kb) 119904 [startup+1190.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 32967 0 0 0 118558 202 0 0 25 0 1 0 1846656060 121462784 28633 4294967295 134512640 135094434 3221224432 3221223120 134554726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 29654 28633 145 145 0 29509 0 [pid=9156] vsize: 118616 Current children cumulated CPU time (s) 1187.61 Current children cumulated vsize (Kb) 120740 [startup+1200.09 s] Raw data (loadavg): 1.00 0.99 0.96 2/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) R 9152 9152 20115 0 -1 0 33281 0 0 0 119554 204 0 0 25 0 1 0 1846656060 122744832 28947 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9156/statm): 29967 28947 145 145 0 29822 0 [pid=9156] vsize: 119868 Current children cumulated CPU time (s) 1197.59 Current children cumulated vsize (Kb) 121992 [startup+1210.1 s] Raw data (loadavg): 1.00 0.99 0.96 1/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) T 9152 9152 20115 0 -1 0 33613 0 0 0 120550 206 0 0 25 0 1 0 1846656060 124108800 29279 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9156/statm): 30300 29279 145 145 0 30155 0 [pid=9156] vsize: 121200 Current children cumulated CPU time (s) 1207.57 Current children cumulated vsize (Kb) 123324 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 0.99 0.96 1/57 9156 Raw data (/proc/9152/stat): 9152 (minisat+_script) S 9151 9152 20115 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846656055 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9152/statm): 531 226 485 147 0 384 0 [pid=9152] vsize: 2124 Raw data (/proc/9156/stat): 9156 (minisat+_64-bit) T 9152 9152 20115 0 -1 0 33613 0 0 0 120550 206 0 0 25 0 1 0 1846656060 124108800 29279 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/9156/statm): 30300 29279 145 145 0 30155 0 [pid=9156] vsize: 121200 Current children cumulated CPU time (s) 1207.57 Current children cumulated vsize (Kb) 123324 Sending SIGTERM to -9152 Sleeping 2 seconds One traced child (pid=9152) ended because it received signal 15 (SIGTERM) One traced child (pid=9156) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.16 CPU time (s): 1207.62 CPU user time (s): 1205.5 CPU system time (s): 2.11868 CPU usage (%): 99.7905 Max. virtual memory (cumulated for all children) (Kb): 123324
ERROR: no interpretation found !