Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod013.opb |
MD5SUM | f118194cabf88b58b64a9e7aec087bc0 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 46012422 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1488 |
Biggest coefficient in the objective function | 375272767488 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 12937590079727 |
Number of bits of the sum of numbers in the objective function | 44 |
Biggest number in a constraint | 375272767488 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 12937590079727 |
Number of bits of the biggest sum of numbers | 44 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.05 |
Number of variables | 1488 |
Total number of constraints | 110 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 48 |
Number of constraints which are nor clauses,nor cardinality constraints | 62 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 240 |
LAUNCH ON wulflinc11 THE 2005-09-19 03:17:21 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2870 boxname=wulflinc11 idbench=526 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f118194cabf88b58b64a9e7aec087bc0 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod013.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod013.opb IDLAUNCH: 2870 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 879376 kB Buffers: 35632 kB Cached: 92224 kB SwapCached: 732 kB Active: 63732 kB Inactive: 66676 kB HighTotal: 131008 kB HighFree: 36988 kB LowTotal: 903652 kB LowFree: 842388 kB SwapTotal: 2097136 kB SwapFree: 2095856 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19100 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:37:31 (client local time) WITH STATUS 10 IN 1207.99 SECONDS stats: 2870 7 1207.99 10
c Parsing PB file... c Converting 76 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############## c -- Clauses(.)/Splits(s): (none) c ---[ 74]---> Sorter-cost: 1234 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 72]---> Sorter-cost: 1234 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 1176 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 1176 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 1176 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 1042 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> BDD-cost: 22 c ---[ 62]---> BDD-cost: 19 c ---[ 61]---> BDD-cost: 20 c ---[ 60]---> BDD-cost: 18 c ---[ 58]---> Sorter-cost: 1897 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> BDD-cost: 18 c ---[ 56]---> BDD-cost: 17 c ---[ 55]---> BDD-cost: 17 c ---[ 54]---> BDD-cost: 16 c ---[ 53]---> BDD-cost: 22 c ---[ 52]---> BDD-cost: 19 c ---[ 51]---> BDD-cost: 20 c ---[ 50]---> BDD-cost: 18 c ---[ 49]---> BDD-cost: 18 c ---[ 48]---> BDD-cost: 17 c ---[ 46]---> Sorter-cost: 1897 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> BDD-cost: 17 c ---[ 44]---> BDD-cost: 16 c ---[ 43]---> BDD-cost: 19 c ---[ 42]---> BDD-cost: 19 c ---[ 41]---> BDD-cost: 20 c ---[ 40]---> BDD-cost: 18 c ---[ 39]---> BDD-cost: 18 c ---[ 38]---> BDD-cost: 17 c ---[ 37]---> BDD-cost: 17 c ---[ 36]---> BDD-cost: 16 c ---[ 34]---> Sorter-cost: 1843 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> BDD-cost: 18 c ---[ 32]---> BDD-cost: 18 c ---[ 31]---> BDD-cost: 18 c ---[ 30]---> BDD-cost: 18 c ---[ 29]---> BDD-cost: 18 c ---[ 28]---> BDD-cost: 17 c ---[ 27]---> BDD-cost: 17 c ---[ 26]---> BDD-cost: 16 c ---[ 25]---> BDD-cost: 17 c ---[ 24]---> BDD-cost: 17 c ---[ 22]---> Sorter-cost: 1843 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> BDD-cost: 17 c ---[ 20]---> BDD-cost: 17 c ---[ 19]---> BDD-cost: 17 c ---[ 18]---> BDD-cost: 17 c ---[ 17]---> BDD-cost: 17 c ---[ 16]---> BDD-cost: 16 c ---[ 15]---> BDD-cost: 16 c ---[ 14]---> BDD-cost: 16 c ---[ 13]---> BDD-cost: 16 c ---[ 12]---> BDD-cost: 16 c ---[ 10]---> Sorter-cost: 1793 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> BDD-cost: 16 c ---[ 8]---> BDD-cost: 16 c ---[ 7]---> BDD-cost: 16 c ---[ 6]---> BDD-cost: 16 c ---[ 4]---> Sorter-cost: 1589 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 1219 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 1234 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 52235 123460 | 17411 0 0 nan | 0.000 % | c | 100 | 52208 123399 | 19152 99 321 3.2 | 8.091 % | c | 250 | 52197 123375 | 21067 248 956 3.9 | 8.107 % | c | 475 | 52169 123313 | 23174 469 2028 4.3 | 8.149 % | c ============================================================================== c [1mFound solution: 83322090[0m c ---[ 0]---> Adder-cost: 5416 maxlim: 164477957 bits: 28/28 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 684 | 89762 257873 | 29920 675 3086 4.6 | 8.149 % | c | 787 | 89607 257520 | 32912 765 3688 4.8 | 6.836 % | c | 937 | 89607 257520 | 36203 915 4406 4.8 | 6.836 % | c | 1162 | 89578 257454 | 39823 1139 5432 4.8 | 6.869 % | c | 1499 | 89445 257150 | 43805 1472 11344 7.7 | 7.032 % | c | 2005 | 89445 257150 | 48186 1978 29991 15.2 | 7.032 % | c ============================================================================== c [1mFound solution: 81983676[0m c ---[ 0]---> Adder-cost: 0 maxlim: 165816371 bits: 28/28 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2474 | 89448 257275 | 29816 2446 37724 15.4 | 7.032 % | c | 2574 | 89318 256978 | 32797 2541 38267 15.1 | 7.250 % | c | 2725 | 89318 256978 | 36077 2692 43881 16.3 | 7.250 % | c | 2950 | 89293 256923 | 39685 2915 45043 15.5 | 7.282 % | c | 3288 | 89293 256923 | 43653 3253 49459 15.2 | 7.282 % | c | 3794 | 89293 256923 | 48018 3759 61354 16.3 | 7.282 % | c | 4553 | 89293 256923 | 52820 4518 84106 18.6 | 7.282 % | c ============================================================================== c [1mFound solution: 74364692[0m c ---[ 0]---> Adder-cost: 0 maxlim: 173435355 bits: 28/28 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4699 | 89303 257166 | 29767 4662 92920 19.9 | 7.282 % | c | 4799 | 89296 257151 | 32743 4761 93439 19.6 | 7.371 % | c | 4949 | 89267 257083 | 36018 4909 95100 19.4 | 7.404 % | c | 5174 | 89267 257083 | 39619 5134 96754 18.8 | 7.404 % | c | 5512 | 89251 257046 | 43581 5468 118879 21.7 | 7.424 % | c ============================================================================== c [1mFound solution: 45615645[0m c ---[ 0]---> Adder-cost: 0 maxlim: 202184402 bits: 28/28 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5630 | 89219 256711 | 29739 5578 124868 22.4 | 7.424 % | c | 5730 | 89219 256711 | 32712 5678 125580 22.1 | 7.500 % | c | 5880 | 89219 256711 | 35984 5828 126740 21.7 | 7.500 % | c | 6106 | 89219 256711 | 39582 6054 128379 21.2 | 7.500 % | c | 6443 | 89203 256659 | 43540 6388 134746 21.1 | 7.513 % | c | 6953 | 89203 256659 | 47894 6898 191637 27.8 | 7.513 % | c | 7712 | 89203 256659 | 52684 7657 202078 26.4 | 7.513 % | c | 8851 | 89203 256659 | 57952 8796 330991 37.6 | 7.513 % | c | 10559 | 89163 256569 | 63748 10501 631221 60.1 | 7.561 % | c | 13121 | 89147 256534 | 70123 13061 758387 58.1 | 7.582 % | c | 16965 | 89147 256534 | 77135 16905 1260176 74.5 | 7.582 % | c | 22731 | 89057 256330 | 84848 22665 1536060 67.8 | 7.700 % | c | 31384 | 88979 256153 | 93333 31313 2170685 69.3 | 7.797 % | c | 44361 | 88979 256153 | 102667 44290 4075055 92.0 | 7.797 % | c | 63823 | 88975 256144 | 112933 63751 7017820 110.1 | 7.801 % | c | 93018 | 88929 256038 | 124227 92942 9549585 102.7 | 7.858 % | c | 136807 | 88909 255994 | 136649 23972 2635704 109.9 | 7.882 % | c | 202492 | 88742 255609 | 150314 89642 8670166 96.7 | 8.082 % | c | 301018 | 88539 255148 | 165346 34282 5339795 155.8 | 8.317 % | c c *** TERMINATED *** s SATISFIABLE v -C1_0x2e__bit_10 C1_0x2e__bit_9 C1_0x2e__bit_8 -C1_0x2e__bit_7 C1_0x2e__bit_6 C1_0x2e__bit_5 -C1_0x2e__bit_4 -C1_0x2e__bit_3 C1_0x2e__bit_2 -C1_0x2e__bit_1 -C1_0x2e__bit0 -C1_0x2e__bit1 C1_0x2e__bit2 C1_0x2e__bit3 C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C1_0x2e__bit13 -C1_0x2e__bit14 -C1_0x2e__bit15 -C1_0x2e__bit16 -C1_0x2e__bit17 -C1_0x2e__bit18 -C1_0x2e__bit19 -C2_0x2e__bit_10 C2_0x2e__bit_9 C2_0x2e__bit_8 C2_0x2e__bit_7 -C2_0x2e__bit_6 C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 C2_0x2e__bit_2 C2_0x2e__bit_1 C2_0x2e__bit0 C2_0x2e__bit1 C2_0x2e__bit2 -C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C2_0x2e__bit13 -C2_0x2e__bit14 -C2_0x2e__bit15 -C2_0x2e__bit16 -C2_0x2e__bit17 -C2_0x2e__bit18 -C2_0x2e__bit19 -C3_0x2e__bit_10 -C3_0x2e__bit_9 -C3_0x2e__bit_8 -C3_0x2e__bit_7 -C3_0x2e__bit_6 -C3_0x2e__bit_5 -C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 -C3_0x2e__bit0 -C3_0x2e__bit1 -C3_0x2e__bit2 -C3_0x2e__bit3 -C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C3_0x2e__bit13 -C3_0x2e__bit14 -C3_0x2e__bit15 -C3_0x2e__bit16 -C3_0x2e__bit17 -C3_0x2e__bit18 -C3_0x2e__bit19 -C4_0x2e__bit_10 -C4_0x2e__bit_9 -C4_0x2e__bit_8 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 C4_0x2e__bit_4 -C4_0x2e__bit_3 C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 -C4_0x2e__bit2 C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C4_0x2e__bit13 -C4_0x2e__bit14 -C4_0x2e__bit15 -C4_0x2e__bit16 -C4_0x2e__bit17 -C4_0x2e__bit18 -C4_0x2e__bit19 -C5_0x2e__bit_10 -C5_0x2e__bit_9 -C5_0x2e__bit_8 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 -C5_0x2e__bit_3 -C5_0x2e__bit_2 -C5_0x2e__bit_1 -C5_0x2e__bit0 -C5_0x2e__bit1 -C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C5_0x2e__bit13 -C5_0x2e__bit14 -C5_0x2e__bit15 -C5_0x2e__bit16 -C5_0x2e__bit17 -C5_0x2e__bit18 -C5_0x2e__bit19 -C6_0x2e__bit_10 -C6_0x2e__bit_9 -C6_0x2e__bit_8 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C6_0x2e__bit13 -C6_0x2e__bit14 -C6_0x2e__bit15 -C6_0x2e__bit16 -C6_0x2e__bit17 -C6_0x2e__bit18 -C6_0x2e__bit19 -C7_0x2e__bit_10 C7_0x2e__bit_9 C7_0x2e__bit_8 C7_0x2e__bit_7 -C7_0x2e__bit_6 C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 C7_0x2e__bit_2 -C7_0x2e__bit_1 -C7_0x2e__bit0 -C7_0x2e__bit1 -C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C7_0x2e__bit13 -C7_0x2e__bit14 -C7_0x2e__bit15 -C7_0x2e__bit16 -C7_0x2e__bit17 -C7_0x2e__bit18 -C7_0x2e__bit19 -C8_0x2e__bit_10 C8_0x2e__bit_9 C8_0x2e__bit_8 C8_0x2e__bit_7 -C8_0x2e__bit_6 C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 -C8_0x2e__bit13 -C8_0x2e__bit14 -C8_0x2e__bit15 -C8_0x2e__bit16 -C8_0x2e__bit17 -C8_0x2e__bit18 -C8_0x2e__bit19 C9_0x2e__bit_10 C9_0x2e__bit_9 -C9_0x2e__bit_8 C9_0x2e__bit_7 C9_0x2e__bit_6 -C9_0x2e__bit_5 -C9_0x2e__bit_4 -C9_0x2e__bit_3 C9_0x2e__bit_2 C9_0x2e__bit_1 C9_0x2e__bit0 C9_0x2e__bit1 -C9_0x2e__bit2 -C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 -C9_0x2e__bit13 -C9_0x2e__bit14 -C9_0x2e__bit15 -C9_0x2e__bit16 -C9_0x2e__bit17 -C9_0x2e__bit18 -C9_0x2e__bit19 -C10_0x2e__bit_10 C10_0x2e__bit_9 -C10_0x2e__bit_8 -C10_0x2e__bit_7 C10_0x2e__bit_6 -C10_0x2e__bit_5 C10_0x2e__bit_4 C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 C10_0x2e__bit0 C10_0x2e__bit1 C10_0x2e__bit2 -C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C10_0x2e__bit13 -C10_0x2e__bit14 -C10_0x2e__bit15 -C10_0x2e__bit16 -C10_0x2e__bit17 -C10_0x2e__bit18 -C10_0x2e__bit19 -C11_0x2e__bit_10 -C11_0x2e__bit_9 -C11_0x2e__bit_8 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 C11_0x2e__bit3 C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 -C11_0x2e__bit13 -C11_0x2e__bit14 -C11_0x2e__bit15 -C11_0x2e__bit16 -C11_0x2e__bit17 -C11_0x2e__bit18 -C11_0x2e__bit19 -C12_0x2e__bit_10 -C12_0x2e__bit_9 -C12_0x2e__bit_8 -C12_0x2e__bit_7 -C12_0x2e__bit_6 -C12_0x2e__bit_5 -C12_0x2e__bit_4 -C12_0x2e__bit_3 -C12_0x2e__bit_2 -C12_0x2e__bit_1 -C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 -C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C12_0x2e__bit13 -C12_0x2e__bit14 -C12_0x2e__bit15 -C12_0x2e__bit16 -C12_0x2e__bit17 -C12_0x2e__bit18 -C12_0x2e__bit19 -C13_0x2e__bit_10 -C13_0x2e__bit_9 -C13_0x2e__bit_8 -C13_0x2e__bit_7 -C13_0x2e__bit_6 -C13_0x2e__bit_5 -C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 -C13_0x2e__bit_1 -C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 -C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C13_0x2e__bit13 -C13_0x2e__bit14 -C13_0x2e__bit15 -C13_0x2e__bit16 -C13_0x2e__bit17 -C13_0x2e__bit18 -C13_0x2e__bit19 -C14_0x2e__bit_10 -C14_0x2e__bit_9 -C14_0x2e__bit_8 C14_0x2e__bit_7 C14_0x2e__bit_6 -C14_0x2e__bit_5 C14_0x2e__bit_4 C14_0x2e__bit_3 -C14_0x2e__bit_2 C14_0x2e__bit_1 C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C14_0x2e__bit13 -C14_0x2e__bit14 -C14_0x2e__bit15 -C14_0x2e__bit16 -C14_0x2e__bit17 -C14_0x2e__bit18 -C14_0x2e__bit19 -C15_0x2e__bit_10 -C15_0x2e__bit_9 -C15_0x2e__bit_8 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C15_0x2e__bit13 -C15_0x2e__bit14 -C15_0x2e__bit15 -C15_0x2e__bit16 -C15_0x2e__bit17 -C15_0x2e__bit18 -C15_0x2e__bit19 C16_0x2e__bit_10 C16_0x2e__bit_9 -C16_0x2e__bit_8 C16_0x2e__bit_7 C16_0x2e__bit_6 C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 -C16_0x2e__bit13 -C16_0x2e__bit14 -C16_0x2e__bit15 -C16_0x2e__bit16 -C16_0x2e__bit17 -C16_0x2e__bit18 -C16_0x2e__bit19 -C17_0x2e__bit_10 -C17_0x2e__bit_9 -C17_0x2e__bit_8 -C17_0x2e__bit_7 -C17_0x2e__bit_6 -C17_0x2e__bit_5 -C17_0x2e__bit_4 -C17_0x2e__bit_3 -C17_0x2e__bit_2 -C17_0x2e__bit_1 -C17_0x2e__bit0 -C17_0x2e__bit1 -C17_0x2e__bit2 -C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 -C17_0x2e__bit13 -C17_0x2e__bit14 -C17_0x2e__bit15 -C17_0x2e__bit16 -C17_0x2e__bit17 -C17_0x2e__bit18 -C17_0x2e__bit19 -C18_0x2e__bit_10 -C18_0x2e__bit_9 -C18_0x2e__bit_8 -C18_0x2e__bit_7 -C18_0x2e__bit_6 -C18_0x2e__bit_5 -C18_0x2e__bit_4 -C18_0x2e__bit_3 -C18_0x2e__bit_2 -C18_0x2e__bit_1 C18_0x2e__bit0 C18_0x2e__bit1 C18_0x2e__bit2 C18_0x2e__bit3 -C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 -C18_0x2e__bit13 -C18_0x2e__bit14 -C18_0x2e__bit15 -C18_0x2e__bit16 -C18_0x2e__bit17 -C18_0x2e__bit18 -C18_0x2e__bit19 -C19_0x2e__bit_10 -C19_0x2e__bit_9 -C19_0x2e__bit_8 -C19_0x2e__bit_7 -C19_0x2e__bit_6 -C19_0x2e__bit_5 -C19_0x2e__bit_4 -C19_0x2e__bit_3 -C19_0x2e__bit_2 -C19_0x2e__bit_1 -C19_0x2e__bit0 -C19_0x2e__bit1 -C19_0x2e__bit2 -C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C19_0x2e__bit13 -C19_0x2e__bit14 -C19_0x2e__bit15 -C19_0x2e__bit16 -C19_0x2e__bit17 -C19_0x2e__bit18 -C19_0x2e__bit19 -C20_0x2e__bit_10 -C20_0x2e__bit_9 -C20_0x2e__bit_8 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C20_0x2e__bit13 -C20_0x2e__bit14 -C20_0x2e__bit15 -C20_0x2e__bit16 -C20_0x2e__bit17 -C20_0x2e__bit18 -C20_0x2e__bit19 -C21_0x2e__bit_10 -C21_0x2e__bit_9 -C21_0x2e__bit_8 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 C21_0x2e__bit0 C21_0x2e__bit1 C21_0x2e__bit2 C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C21_0x2e__bit13 -C21_0x2e__bit14 -C21_0x2e__bit15 -C21_0x2e__bit16 -C21_0x2e__bit17 -C21_0x2e__bit18 -C21_0x2e__bit19 -C22_0x2e__bit_10 -C22_0x2e__bit_9 -C22_0x2e__bit_8 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C22_0x2e__bit13 -C22_0x2e__bit14 -C22_0x2e__bit15 -C22_0x2e__bit16 -C22_0x2e__bit17 -C22_0x2e__bit18 -C22_0x2e__bit19 -C23_0x2e__bit_10 -C23_0x2e__bit_9 -C23_0x2e__bit_8 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C23_0x2e__bit13 -C23_0x2e__bit14 -C23_0x2e__bit15 -C23_0x2e__bit16 -C23_0x2e__bit17 -C23_0x2e__bit18 -C23_0x2e__bit19 -C24_0x2e__bit_10 -C24_0x2e__bit_9 -C24_0x2e__bit_8 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C24_0x2e__bit13 -C24_0x2e__bit14 -C24_0x2e__bit15 -C24_0x2e__bit16 -C24_0x2e__bit17 -C24_0x2e__bit18 -C24_0x2e__bit19 -C25_0x2e__bit_10 -C25_0x2e__bit_9 -C25_0x2e__bit_8 -C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C25_0x2e__bit13 -C25_0x2e__bit14 -C25_0x2e__bit15 -C25_0x2e__bit16 -C25_0x2e__bit17 -C25_0x2e__bit18 -C25_0x2e__bit19 -C26_0x2e__bit_10 -C26_0x2e__bit_9 -C26_0x2e__bit_8 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C26_0x2e__bit13 -C26_0x2e__bit14 -C26_0x2e__bit15 -C26_0x2e__bit16 -C26_0x2e__bit17 -C26_0x2e__bit18 -C26_0x2e__bit19 -C27_0x2e__bit_10 -C27_0x2e__bit_9 -C27_0x2e__bit_8 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 -C27_0x2e__bit13 -C27_0x2e__bit14 -C27_0x2e__bit15 -C27_0x2e__bit16 -C27_0x2e__bit17 -C27_0x2e__bit18 -C27_0x2e__bit19 -C28_0x2e__bit_10 -C28_0x2e__bit_9 -C28_0x2e__bit_8 -C28_0x2e__bit_7 -C28_0x2e__bit_6 -C28_0x2e__bit_5 C28_0x2e__bit_4 C28_0x2e__bit_3 -C28_0x2e__bit_2 C28_0x2e__bit_1 C28_0x2e__bit0 C28_0x2e__bit1 -C28_0x2e__bit2 C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C28_0x2e__bit13 -C28_0x2e__bit14 -C28_0x2e__bit15 -C28_0x2e__bit16 -C28_0x2e__bit17 -C28_0x2e__bit18 -C28_0x2e__bit19 -C29_0x2e__bit_10 -C29_0x2e__bit_9 -C29_0x2e__bit_8 -C29_0x2e__bit_7 -C29_0x2e__bit_6 -C29_0x2e__bit_5 -C29_0x2e__bit_4 -C29_0x2e__bit_3 -C29_0x2e__bit_2 -C29_0x2e__bit_1 -C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C29_0x2e__bit13 -C29_0x2e__bit14 -C29_0x2e__bit15 -C29_0x2e__bit16 -C29_0x2e__bit17 -C29_0x2e__bit18 -C29_0x2e__bit19 -C30_0x2e__bit_10 C30_0x2e__bit_9 -C30_0x2e__bit_8 C30_0x2e__bit_7 C30_0x2e__bit_6 C30_0x2e__bit_5 C30_0x2e__bit_4 C30_0x2e__bit_3 C30_0x2e__bit_2 C30_0x2e__bit_1 C30_0x2e__bit0 C30_0x2e__bit1 C30_0x2e__bit2 -C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C30_0x2e__bit13 -C30_0x2e__bit14 -C30_0x2e__bit15 -C30_0x2e__bit16 -C30_0x2e__bit17 -C30_0x2e__bit18 -C30_0x2e__bit19 -C31_0x2e__bit_10 -C31_0x2e__bit_9 -C31_0x2e__bit_8 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 -C31_0x2e__bit1 -C31_0x2e__bit2 -C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C31_0x2e__bit13 -C31_0x2e__bit14 -C31_0x2e__bit15 -C31_0x2e__bit16 -C31_0x2e__bit17 -C31_0x2e__bit18 -C31_0x2e__bit19 -C32_0x2e__bit_10 C32_0x2e__bit_9 C32_0x2e__bit_8 -C32_0x2e__bit_7 -C32_0x2e__bit_6 -C32_0x2e__bit_5 C32_0x2e__bit_4 -C32_0x2e__bit_3 C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 -C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C32_0x2e__bit13 -C32_0x2e__bit14 -C32_0x2e__bit15 -C32_0x2e__bit16 -C32_0x2e__bit17 -C32_0x2e__bit18 -C32_0x2e__bit19 -C33_0x2e__bit_10 -C33_0x2e__bit_9 -C33_0x2e__bit_8 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 -C33_0x2e__bit_4 -C33_0x2e__bit_3 -C33_0x2e__bit_2 -C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C33_0x2e__bit13 -C33_0x2e__bit14 -C33_0x2e__bit15 -C33_0x2e__bit16 -C33_0x2e__bit17 -C33_0x2e__bit18 -C33_0x2e__bit19 -C34_0x2e__bit_10 -C34_0x2e__bit_9 -C34_0x2e__bit_8 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 -C34_0x2e__bit_1 -C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C34_0x2e__bit13 -C34_0x2e__bit14 -C34_0x2e__bit15 -C34_0x2e__bit16 -C34_0x2e__bit17 -C34_0x2e__bit18 -C34_0x2e__bit19 -C35_0x2e__bit_10 -C35_0x2e__bit_9 -C35_0x2e__bit_8 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 -C35_0x2e__bit13 -C35_0x2e__bit14 -C35_0x2e__bit15 -C35_0x2e__bit16 -C35_0x2e__bit17 -C35_0x2e__bit18 -C35_0x2e__bit19 -C36_0x2e__bit_10 -C36_0x2e__bit_9 -C36_0x2e__bit_8 -C36_0x2e__bit_7 -C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 -C36_0x2e__bit_1 -C36_0x2e__bit0 -C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C36_0x2e__bit13 -C36_0x2e__bit14 -C36_0x2e__bit15 -C36_0x2e__bit16 -C36_0x2e__bit17 -C36_0x2e__bit18 -C36_0x2e__bit19 -C37_0x2e__bit_10 -C37_0x2e__bit_9 -C37_0x2e__bit_8 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 -C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 -C37_0x2e__bit0 -C37_0x2e__bit1 -C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C37_0x2e__bit13 -C37_0x2e__bit14 -C37_0x2e__bit15 -C37_0x2e__bit16 -C37_0x2e__bit17 -C37_0x2e__bit18 -C37_0x2e__bit19 -C38_0x2e__bit_10 C38_0x2e__bit_9 C38_0x2e__bit_8 C38_0x2e__bit_7 -C38_0x2e__bit_6 C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 C38_0x2e__bit_2 -C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38_0x2e__bit10 -C38_0x2e__bit11 -C38_0x2e__bit12 -C38_0x2e__bit13 -C38_0x2e__bit14 -C38_0x2e__bit15 -C38_0x2e__bit16 -C38_0x2e__bit17 -C38_0x2e__bit18 -C38_0x2e__bit19 -C39_0x2e__bit_10 C39_0x2e__bit_9 -C39_0x2e__bit_8 -C39_0x2e__bit_7 C39_0x2e__bit_6 -C39_0x2e__bit_5 C39_0x2e__bit_4 C39_0x2e__bit_3 -C39_0x2e__bit_2 C39_0x2e__bit_1 C39_0x2e__bit0 -C39_0x2e__bit1 -C39_0x2e__bit2 C39_0x2e__bit3 -C39_0x2e__bit4 -C39_0x2e__bit5 -C39_0x2e__bit6 -C39_0x2e__bit7 -C39_0x2e__bit8 -C39_0x2e__bit9 -C39_0x2e__bit10 -C39_0x2e__bit11 -C39_0x2e__bit12 -C39_0x2e__bit13 -C39_0x2e__bit14 -C39_0x2e__bit15 -C39_0x2e__bit16 -C39_0x2e__bit17 -C39_0x2e__bit18 -C39_0x2e__bit19 -C40_0x2e__bit_10 -C40_0x2e__bit_9 -C40_0x2e__bit_8 -C40_0x2e__bit_7 -C40_0x2e__bit_6 -C40_0x2e__bit_5 -C40_0x2e__bit_4 -C40_0x2e__bit_3 -C40_0x2e__bit_2 -C40_0x2e__bit_1 -C40_0x2e__bit0 -C40_0x2e__bit1 -C40_0x2e__bit2 -C40_0x2e__bit3 -C40_0x2e__bit4 -C40_0x2e__bit5 -C40_0x2e__bit6 -C40_0x2e__bit7 -C40_0x2e__bit8 -C40_0x2e__bit9 -C40_0x2e__bit10 -C40_0x2e__bit11 -C40_0x2e__bit12 -C40_0x2e__bit13 -C40_0x2e__bit14 -C40_0x2e__bit15 -C40_0x2e__bit16 -C40_0x2e__bit17 -C40_0x2e__bit18 -C40_0x2e__bit19 C41_0x2e__bit_10 C41_0x2e__bit_9 C41_0x2e__bit_8 C41_0x2e__bit_7 -C41_0x2e__bit_6 C41_0x2e__bit_5 -C41_0x2e__bit_4 C41_0x2e__bit_3 C41_0x2e__bit_2 C41_0x2e__bit_1 -C41_0x2e__bit0 C41_0x2e__bit1 -C41_0x2e__bit2 -C41_0x2e__bit3 -C41_0x2e__bit4 -C41_0x2e__bit5 -C41_0x2e__bit6 -C41_0x2e__bit7 -C41_0x2e__bit8 -C41_0x2e__bit9 -C41_0x2e__bit10 -C41_0x2e__bit11 -C41_0x2e__bit12 -C41_0x2e__bit13 -C41_0x2e__bit14 -C41_0x2e__bit15 -C41_0x2e__bit16 -C41_0x2e__bit17 -C41_0x2e__bit18 -C41_0x2e__bit19 -C42_0x2e__bit_10 -C42_0x2e__bit_9 -C42_0x2e__bit_8 -C42_0x2e__bit_7 -C42_0x2e__bit_6 -C42_0x2e__bit_5 -C42_0x2e__bit_4 -C42_0x2e__bit_3 -C42_0x2e__bit_2 -C42_0x2e__bit_1 -C42_0x2e__bit0 -C42_0x2e__bit1 -C42_0x2e__bit2 -C42_0x2e__bit3 -C42_0x2e__bit4 -C42_0x2e__bit5 -C42_0x2e__bi
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/24302/stat): 24302 (minisat+_script) R 24301 24302 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1788359053 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24302/statm): 174 3 169 147 0 27 0 [pid=24302] 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=24303 New process pid=24304 New process pid=24305 execve syscall for /bin/sed executable One traced child (pid=24304) 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=24305) exited with status: 0 One traced child (pid=24303) exited with status: 0 New process pid=24306 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-mod013.opb [startup+10.0038 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5009 0 0 0 964 17 0 0 25 0 1 0 1788359058 19259392 4289 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 4702 4289 145 145 0 4557 0 [pid=24306] vsize: 18808 Current children cumulated CPU time (s) 9.82 Current children cumulated vsize (Kb) 20932 [startup+20.0045 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5193 0 0 0 1961 18 0 0 25 0 1 0 1788359058 19726336 4393 4294967295 134512640 135094434 3221224432 3221222432 134677059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 4816 4393 145 145 0 4671 0 [pid=24306] vsize: 19264 Current children cumulated CPU time (s) 19.8 Current children cumulated vsize (Kb) 21388 [startup+30.0063 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5419 0 0 0 2958 19 0 0 25 0 1 0 1788359058 20111360 4506 4294967295 134512640 135094434 3221224432 3221221984 134599924 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 4910 4506 145 145 0 4765 0 [pid=24306] vsize: 19640 Current children cumulated CPU time (s) 29.78 Current children cumulated vsize (Kb) 21764 [startup+40.0071 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5551 0 0 0 3956 21 0 0 25 0 1 0 1788359058 20295680 4557 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 4955 4557 145 145 0 4810 0 [pid=24306] vsize: 19820 Current children cumulated CPU time (s) 39.78 Current children cumulated vsize (Kb) 21944 [startup+50.0079 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 5851 0 0 0 4951 23 0 0 25 0 1 0 1788359058 21544960 4857 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 5260 4857 145 145 0 5115 0 [pid=24306] vsize: 21040 Current children cumulated CPU time (s) 49.75 Current children cumulated vsize (Kb) 23164 [startup+60.0087 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) T 24302 24302 9854 0 -1 0 6424 0 0 0 5941 27 0 0 25 0 1 0 1788359058 23883776 5430 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/24306/statm): 5831 5430 145 145 0 5686 0 [pid=24306] vsize: 23324 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 25448 [startup+70.0095 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 6814 0 0 0 6934 31 0 0 25 0 1 0 1788359058 25526272 5820 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 6232 5820 145 145 0 6087 0 [pid=24306] vsize: 24928 Current children cumulated CPU time (s) 69.66 Current children cumulated vsize (Kb) 27052 [startup+80.0113 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 7183 0 0 0 7927 33 0 0 25 0 1 0 1788359058 27017216 6189 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 6596 6189 145 145 0 6451 0 [pid=24306] vsize: 26384 Current children cumulated CPU time (s) 79.61 Current children cumulated vsize (Kb) 28508 [startup+90.0121 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 7541 0 0 0 8921 36 0 0 25 0 1 0 1788359058 28467200 6547 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 6950 6547 145 145 0 6805 0 [pid=24306] vsize: 27800 Current children cumulated CPU time (s) 89.58 Current children cumulated vsize (Kb) 29924 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 8032 0 0 0 9912 39 0 0 25 0 1 0 1788359058 30580736 7038 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 7466 7038 145 145 0 7321 0 [pid=24306] vsize: 29864 Current children cumulated CPU time (s) 99.52 Current children cumulated vsize (Kb) 31988 [startup+110.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 8632 0 0 0 10904 43 0 0 25 0 1 0 1788359058 33021952 7638 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 8062 7638 145 145 0 7917 0 [pid=24306] vsize: 32248 Current children cumulated CPU time (s) 109.48 Current children cumulated vsize (Kb) 34372 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 9359 0 0 0 11893 48 0 0 25 0 1 0 1788359058 35983360 8365 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 8785 8365 145 145 0 8640 0 [pid=24306] vsize: 35140 Current children cumulated CPU time (s) 119.42 Current children cumulated vsize (Kb) 37264 [startup+130.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 9847 0 0 0 12885 52 0 0 25 0 1 0 1788359058 37965824 8853 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 9269 8853 145 145 0 9124 0 [pid=24306] vsize: 37076 Current children cumulated CPU time (s) 129.38 Current children cumulated vsize (Kb) 39200 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 9991 0 0 0 13882 53 0 0 25 0 1 0 1788359058 38547456 8997 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 9411 8997 145 145 0 9266 0 [pid=24306] vsize: 37644 Current children cumulated CPU time (s) 139.36 Current children cumulated vsize (Kb) 39768 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 10296 0 0 0 14876 56 0 0 25 0 1 0 1788359058 39784448 9302 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 9713 9302 145 145 0 9568 0 [pid=24306] vsize: 38852 Current children cumulated CPU time (s) 149.33 Current children cumulated vsize (Kb) 40976 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 11195 0 0 0 15863 61 0 0 25 0 1 0 1788359058 43446272 10201 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 10607 10201 145 145 0 10462 0 [pid=24306] vsize: 42428 Current children cumulated CPU time (s) 159.25 Current children cumulated vsize (Kb) 44552 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 12140 0 0 0 16849 68 0 0 25 0 1 0 1788359058 47296512 11146 4294967295 134512640 135094434 3221224432 3221223024 134557306 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 11547 11146 145 145 0 11402 0 [pid=24306] vsize: 46188 Current children cumulated CPU time (s) 169.18 Current children cumulated vsize (Kb) 48312 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) T 24302 24302 9854 0 -1 0 12964 0 0 0 17836 73 0 0 25 0 1 0 1788359058 50655232 11970 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/24306/statm): 12367 11970 145 145 0 12222 0 [pid=24306] vsize: 49468 Current children cumulated CPU time (s) 179.1 Current children cumulated vsize (Kb) 51592 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 13396 0 0 0 18828 77 0 0 25 0 1 0 1788359058 52666368 12402 4294967295 134512640 135094434 3221224432 3221223080 134556677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 12858 12402 145 145 0 12713 0 [pid=24306] vsize: 51432 Current children cumulated CPU time (s) 189.06 Current children cumulated vsize (Kb) 53556 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 13663 0 0 0 19823 79 0 0 25 0 1 0 1788359058 53747712 12669 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 13122 12669 145 145 0 12977 0 [pid=24306] vsize: 52488 Current children cumulated CPU time (s) 199.03 Current children cumulated vsize (Kb) 54612 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14016 0 0 0 20817 82 0 0 25 0 1 0 1788359058 55185408 13022 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 13473 13022 145 145 0 13328 0 [pid=24306] vsize: 53892 Current children cumulated CPU time (s) 209 Current children cumulated vsize (Kb) 56016 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14331 0 0 0 21811 85 0 0 25 0 1 0 1788359058 56467456 13337 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 13786 13337 145 145 0 13641 0 [pid=24306] vsize: 55144 Current children cumulated CPU time (s) 218.97 Current children cumulated vsize (Kb) 57268 [startup+230.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14621 0 0 0 22805 87 0 0 25 0 1 0 1788359058 57643008 13627 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 14073 13627 145 145 0 13928 0 [pid=24306] vsize: 56292 Current children cumulated CPU time (s) 228.93 Current children cumulated vsize (Kb) 58416 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 14961 0 0 0 23800 89 0 0 25 0 1 0 1788359058 59023360 13967 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 14410 13967 145 145 0 14265 0 [pid=24306] vsize: 57640 Current children cumulated CPU time (s) 238.9 Current children cumulated vsize (Kb) 59764 [startup+250.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15237 0 0 0 24796 91 0 0 25 0 1 0 1788359058 60137472 14243 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 14682 14243 145 145 0 14537 0 [pid=24306] vsize: 58728 Current children cumulated CPU time (s) 248.88 Current children cumulated vsize (Kb) 60852 [startup+260.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15602 0 0 0 25791 93 0 0 25 0 1 0 1788359058 61616128 14608 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 15043 14608 145 145 0 14898 0 [pid=24306] vsize: 60172 Current children cumulated CPU time (s) 258.85 Current children cumulated vsize (Kb) 62296 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15781 0 0 0 26788 94 0 0 25 0 1 0 1788359058 62341120 14787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 15220 14787 145 145 0 15075 0 [pid=24306] vsize: 60880 Current children cumulated CPU time (s) 268.83 Current children cumulated vsize (Kb) 63004 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 15896 0 0 0 27785 95 0 0 25 0 1 0 1788359058 62812160 14902 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 15335 14902 145 145 0 15190 0 [pid=24306] vsize: 61340 Current children cumulated CPU time (s) 278.81 Current children cumulated vsize (Kb) 63464 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16011 0 0 0 28784 97 0 0 25 0 1 0 1788359058 63275008 15017 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 15448 15017 145 145 0 15303 0 [pid=24306] vsize: 61792 Current children cumulated CPU time (s) 288.82 Current children cumulated vsize (Kb) 63916 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16160 0 0 0 29781 98 0 0 25 0 1 0 1788359058 63877120 15166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 15595 15166 145 145 0 15450 0 [pid=24306] vsize: 62380 Current children cumulated CPU time (s) 298.8 Current children cumulated vsize (Kb) 64504 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16351 0 0 0 30777 99 0 0 25 0 1 0 1788359058 64651264 15357 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 15784 15357 145 145 0 15639 0 [pid=24306] vsize: 63136 Current children cumulated CPU time (s) 308.77 Current children cumulated vsize (Kb) 65260 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16578 0 0 0 31773 101 0 0 25 0 1 0 1788359058 65576960 15584 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 16010 15584 145 145 0 15865 0 [pid=24306] vsize: 64040 Current children cumulated CPU time (s) 318.75 Current children cumulated vsize (Kb) 66164 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 16978 0 0 0 32766 104 0 0 25 0 1 0 1788359058 67198976 15984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 16406 15984 145 145 0 16261 0 [pid=24306] vsize: 65624 Current children cumulated CPU time (s) 328.71 Current children cumulated vsize (Kb) 67748 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 17337 0 0 0 33759 107 0 0 25 0 1 0 1788359058 68661248 16343 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 16763 16343 145 145 0 16618 0 [pid=24306] vsize: 67052 Current children cumulated CPU time (s) 338.67 Current children cumulated vsize (Kb) 69176 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 17677 0 0 0 34753 109 0 0 25 0 1 0 1788359058 70041600 16683 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 17100 16683 145 145 0 16955 0 [pid=24306] vsize: 68400 Current children cumulated CPU time (s) 348.63 Current children cumulated vsize (Kb) 70524 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 17976 0 0 0 35748 111 0 0 25 0 1 0 1788359058 71258112 16982 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 17397 16982 145 145 0 17252 0 [pid=24306] vsize: 69588 Current children cumulated CPU time (s) 358.6 Current children cumulated vsize (Kb) 71712 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 18282 0 0 0 36743 114 0 0 25 0 1 0 1788359058 72503296 17288 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 17701 17288 145 145 0 17556 0 [pid=24306] vsize: 70804 Current children cumulated CPU time (s) 368.58 Current children cumulated vsize (Kb) 72928 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 18592 0 0 0 37738 116 0 0 25 0 1 0 1788359058 73768960 17598 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 18010 17598 145 145 0 17865 0 [pid=24306] vsize: 72040 Current children cumulated CPU time (s) 378.55 Current children cumulated vsize (Kb) 74164 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 18905 0 0 0 38733 118 0 0 25 0 1 0 1788359058 75042816 17911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 18321 17911 145 145 0 18176 0 [pid=24306] vsize: 73284 Current children cumulated CPU time (s) 388.52 Current children cumulated vsize (Kb) 75408 [startup+400.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 19229 0 0 0 39727 121 0 0 25 0 1 0 1788359058 76369920 18235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 18645 18235 145 145 0 18500 0 [pid=24306] vsize: 74580 Current children cumulated CPU time (s) 398.49 Current children cumulated vsize (Kb) 76704 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 19539 0 0 0 40720 123 0 0 25 0 1 0 1788359058 77635584 18545 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 18954 18545 145 145 0 18809 0 [pid=24306] vsize: 75816 Current children cumulated CPU time (s) 408.44 Current children cumulated vsize (Kb) 77940 [startup+420.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 19875 0 0 0 41715 126 0 0 25 0 1 0 1788359058 79003648 18881 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 19288 18881 145 145 0 19143 0 [pid=24306] vsize: 77152 Current children cumulated CPU time (s) 418.42 Current children cumulated vsize (Kb) 79276 [startup+430.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20110 0 0 0 42711 127 0 0 25 0 1 0 1788359058 79958016 19116 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 19521 19116 145 145 0 19376 0 [pid=24306] vsize: 78084 Current children cumulated CPU time (s) 428.39 Current children cumulated vsize (Kb) 80208 [startup+440.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20377 0 0 0 43705 129 0 0 25 0 1 0 1788359058 81043456 19383 4294967295 134512640 135094434 3221224432 3221223024 134551692 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 19786 19383 145 145 0 19641 0 [pid=24306] vsize: 79144 Current children cumulated CPU time (s) 438.35 Current children cumulated vsize (Kb) 81268 [startup+450.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 44700 131 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221222912 134781309 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 448.32 Current children cumulated vsize (Kb) 82996 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 45700 131 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 458.32 Current children cumulated vsize (Kb) 82996 [startup+470.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 46699 131 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 468.31 Current children cumulated vsize (Kb) 82996 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 47698 132 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223104 134555260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 478.31 Current children cumulated vsize (Kb) 82996 [startup+490.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 48698 132 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 488.31 Current children cumulated vsize (Kb) 82996 [startup+500.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 49698 133 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 498.32 Current children cumulated vsize (Kb) 82996 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 50697 133 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 508.31 Current children cumulated vsize (Kb) 82996 [startup+520.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 51697 134 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 518.32 Current children cumulated vsize (Kb) 82996 [startup+530.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 52696 134 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 528.31 Current children cumulated vsize (Kb) 82996 [startup+540.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 53696 134 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 538.31 Current children cumulated vsize (Kb) 82996 [startup+550.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 54696 135 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 548.32 Current children cumulated vsize (Kb) 82996 [startup+560.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 55695 135 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 558.31 Current children cumulated vsize (Kb) 82996 [startup+570.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 56695 136 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 568.32 Current children cumulated vsize (Kb) 82996 [startup+580.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 57694 136 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 578.31 Current children cumulated vsize (Kb) 82996 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 58694 136 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 588.31 Current children cumulated vsize (Kb) 82996 [startup+600.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 59692 138 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 598.31 Current children cumulated vsize (Kb) 82996 [startup+610.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 60691 139 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 608.31 Current children cumulated vsize (Kb) 82996 [startup+620.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 61691 140 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 618.32 Current children cumulated vsize (Kb) 82996 [startup+630.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 62690 140 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 628.31 Current children cumulated vsize (Kb) 82996 [startup+640.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 63689 141 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 638.31 Current children cumulated vsize (Kb) 82996 [startup+650.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 64689 141 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 648.31 Current children cumulated vsize (Kb) 82996 [startup+660.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 65688 142 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 658.31 Current children cumulated vsize (Kb) 82996 [startup+670.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 66688 142 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 668.31 Current children cumulated vsize (Kb) 82996 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20682 0 0 0 67687 143 0 0 25 0 1 0 1788359058 82812928 19688 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19688 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 678.31 Current children cumulated vsize (Kb) 82996 [startup+690.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 68687 144 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 688.32 Current children cumulated vsize (Kb) 82996 [startup+700.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 69687 144 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223016 134552439 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 698.32 Current children cumulated vsize (Kb) 82996 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 70686 144 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 708.31 Current children cumulated vsize (Kb) 82996 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 71686 145 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 718.32 Current children cumulated vsize (Kb) 82996 [startup+730.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 72685 145 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 728.31 Current children cumulated vsize (Kb) 82996 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 73685 146 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 738.32 Current children cumulated vsize (Kb) 82996 [startup+750.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 74685 146 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 748.32 Current children cumulated vsize (Kb) 82996 [startup+760.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 75684 146 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 758.31 Current children cumulated vsize (Kb) 82996 [startup+770.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 76684 147 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 768.32 Current children cumulated vsize (Kb) 82996 [startup+780.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 77684 147 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 778.32 Current children cumulated vsize (Kb) 82996 [startup+790.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 78683 148 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 788.32 Current children cumulated vsize (Kb) 82996 [startup+800.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 79683 148 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 798.32 Current children cumulated vsize (Kb) 82996 [startup+810.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 80683 148 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 808.32 Current children cumulated vsize (Kb) 82996 [startup+820.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20683 0 0 0 81682 149 0 0 25 0 1 0 1788359058 82812928 19689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19689 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 818.32 Current children cumulated vsize (Kb) 82996 [startup+830.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20684 0 0 0 82681 150 0 0 25 0 1 0 1788359058 82812928 19690 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19690 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 828.32 Current children cumulated vsize (Kb) 82996 [startup+840.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20684 0 0 0 83681 151 0 0 25 0 1 0 1788359058 82812928 19690 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19690 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 838.33 Current children cumulated vsize (Kb) 82996 [startup+850.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20686 0 0 0 84680 151 0 0 25 0 1 0 1788359058 82812928 19692 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19692 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 848.32 Current children cumulated vsize (Kb) 82996 [startup+860.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20688 0 0 0 85680 151 0 0 25 0 1 0 1788359058 82812928 19694 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19694 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 858.32 Current children cumulated vsize (Kb) 82996 [startup+870.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20690 0 0 0 86680 152 0 0 25 0 1 0 1788359058 82812928 19696 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19696 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 868.33 Current children cumulated vsize (Kb) 82996 [startup+880.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20692 0 0 0 87679 152 0 0 25 0 1 0 1788359058 82812928 19698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19698 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 878.32 Current children cumulated vsize (Kb) 82996 [startup+890.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20695 0 0 0 88679 153 0 0 25 0 1 0 1788359058 82812928 19701 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20218 19701 145 145 0 20073 0 [pid=24306] vsize: 80872 Current children cumulated CPU time (s) 888.33 Current children cumulated vsize (Kb) 82996 [startup+900.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 20870 0 0 0 89676 154 0 0 25 0 1 0 1788359058 83521536 19876 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 20391 19876 145 145 0 20246 0 [pid=24306] vsize: 81564 Current children cumulated CPU time (s) 898.31 Current children cumulated vsize (Kb) 83688 [startup+910.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 21758 0 0 0 90663 160 0 0 25 0 1 0 1788359058 87146496 20764 4294967295 134512640 135094434 3221224432 3221223024 134557055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 21276 20764 145 145 0 21131 0 [pid=24306] vsize: 85104 Current children cumulated CPU time (s) 908.24 Current children cumulated vsize (Kb) 87228 [startup+920.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 22101 0 0 0 91659 162 0 0 25 0 1 0 1788359058 88543232 21107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 21617 21107 145 145 0 21472 0 [pid=24306] vsize: 86468 Current children cumulated CPU time (s) 918.22 Current children cumulated vsize (Kb) 88592 [startup+930.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 22222 0 0 0 92656 163 0 0 25 0 1 0 1788359058 89030656 21228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 21736 21228 145 145 0 21591 0 [pid=24306] vsize: 86944 Current children cumulated CPU time (s) 928.2 Current children cumulated vsize (Kb) 89068 [startup+940.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 22696 0 0 0 93649 167 0 0 25 0 1 0 1788359058 90959872 21702 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 22207 21702 145 145 0 22062 0 [pid=24306] vsize: 88828 Current children cumulated CPU time (s) 938.17 Current children cumulated vsize (Kb) 90952 [startup+950.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 23616 0 0 0 94632 173 0 0 25 0 1 0 1788359058 94707712 22622 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 23122 22622 145 145 0 22977 0 [pid=24306] vsize: 92488 Current children cumulated CPU time (s) 948.06 Current children cumulated vsize (Kb) 94612 [startup+960.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 24443 0 0 0 95618 180 0 0 25 0 1 0 1788359058 98070528 23449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 23943 23449 145 145 0 23798 0 [pid=24306] vsize: 95772 Current children cumulated CPU time (s) 957.99 Current children cumulated vsize (Kb) 97896 [startup+970.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25236 0 0 0 96603 186 0 0 25 0 1 0 1788359058 101298176 24242 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24306/statm): 24731 24242 145 145 0 24586 0 [pid=24306] vsize: 98924 Current children cumulated CPU time (s) 967.9 Current children cumulated vsize (Kb) 101048 [startup+980.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 97600 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 977.88 Current children cumulated vsize (Kb) 101744 [startup+990.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 98601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 987.89 Current children cumulated vsize (Kb) 101744 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 99601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 997.89 Current children cumulated vsize (Kb) 101744 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 100601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1007.89 Current children cumulated vsize (Kb) 101744 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 101601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1017.89 Current children cumulated vsize (Kb) 101744 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 102601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1027.89 Current children cumulated vsize (Kb) 101744 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 103601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1037.89 Current children cumulated vsize (Kb) 101744 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 104601 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1047.89 Current children cumulated vsize (Kb) 101744 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 105602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1057.9 Current children cumulated vsize (Kb) 101744 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 106602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1067.9 Current children cumulated vsize (Kb) 101744 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 107602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1077.9 Current children cumulated vsize (Kb) 101744 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 108602 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1087.9 Current children cumulated vsize (Kb) 101744 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 109603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1097.91 Current children cumulated vsize (Kb) 101744 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 110603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1107.91 Current children cumulated vsize (Kb) 101744 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 111603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1117.91 Current children cumulated vsize (Kb) 101744 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 112603 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1127.91 Current children cumulated vsize (Kb) 101744 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 113604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1137.92 Current children cumulated vsize (Kb) 101744 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 114604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1147.92 Current children cumulated vsize (Kb) 101744 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 115604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1157.92 Current children cumulated vsize (Kb) 101744 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 116604 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1167.92 Current children cumulated vsize (Kb) 101744 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 117605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1177.93 Current children cumulated vsize (Kb) 101744 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 118605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1187.93 Current children cumulated vsize (Kb) 101744 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 119605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1197.93 Current children cumulated vsize (Kb) 101744 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 120605 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1207.93 Current children cumulated vsize (Kb) 101744 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 24306 Raw data (/proc/24302/stat): 24302 (minisat+_script) S 24301 24302 9854 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1788359053 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24302/statm): 531 226 485 147 0 384 0 [pid=24302] vsize: 2124 Raw data (/proc/24306/stat): 24306 (minisat+_64-bit) R 24302 24302 9854 0 -1 0 25410 0 0 0 120606 187 0 0 25 0 1 0 1788359058 102010880 24416 4294967295 134512640 135094434 3221224432 3221223056 134557658 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24306/statm): 24905 24416 145 145 0 24760 0 [pid=24306] vsize: 99620 Current children cumulated CPU time (s) 1207.94 Current children cumulated vsize (Kb) 101744 Sending SIGTERM to -24302 Sleeping 2 seconds One traced child (pid=24302) ended because it received signal 15 (SIGTERM) One traced child (pid=24306) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.18 CPU time (s): 1207.99 CPU user time (s): 1206.06 CPU system time (s): 1.92471 CPU usage (%): 99.8187 Max. virtual memory (cumulated for all children) (Kb): 101744
ERROR: no interpretation found !