Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-rgn.opb |
MD5SUM | 4cc62e621e04c5a4e55edc3240fa3357 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 537600 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1160 |
Biggest coefficient in the objective function | 196608 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 15892320 |
Number of bits of the sum of numbers in the objective function | 24 |
Biggest number in a constraint | 25600000000 |
Number of bits of the biggest number in a constraint | 35 |
Biggest sum of numbers in a constraint | 232836875088 |
Number of bits of the biggest sum of numbers | 38 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1249.96 |
Number of variables | 1260 |
Total number of constraints | 204 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 104 |
Number of constraints which are nor clauses,nor cardinality constraints | 100 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 127 |
LAUNCH ON wulflinc20 THE 2005-09-19 18:08:23 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3006 boxname=wulflinc20 idbench=662 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4cc62e621e04c5a4e55edc3240fa3357 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-rgn.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-rgn.opb IDLAUNCH: 3006 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 878052 kB Buffers: 40572 kB Cached: 84940 kB SwapCached: 832 kB Active: 71068 kB Inactive: 57112 kB HighTotal: 131008 kB HighFree: 42728 kB LowTotal: 903652 kB LowFree: 835324 kB SwapTotal: 2097892 kB SwapFree: 2096604 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 22772 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:28:33 (client local time) WITH STATUS 10 IN 1209.11 SECONDS stats: 3006 7 1209.11 10
c Parsing PB file... c Converting 124 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): (none) c ---[ 123]---> BDD-cost: 16 c ---[ 122]---> BDD-cost: 16 c ---[ 121]---> BDD-cost: 16 c ---[ 120]---> BDD-cost: 16 c ---[ 119]---> BDD-cost: 16 c ---[ 118]---> BDD-cost: 16 c ---[ 117]---> BDD-cost: 16 c ---[ 116]---> BDD-cost: 16 c ---[ 115]---> BDD-cost: 16 c ---[ 114]---> BDD-cost: 16 c ---[ 113]---> BDD-cost: 16 c ---[ 112]---> BDD-cost: 16 c ---[ 111]---> BDD-cost: 16 c ---[ 110]---> BDD-cost: 16 c ---[ 109]---> BDD-cost: 16 c ---[ 108]---> BDD-cost: 16 c ---[ 107]---> BDD-cost: 16 c ---[ 106]---> BDD-cost: 16 c ---[ 105]---> BDD-cost: 16 c ---[ 104]---> BDD-cost: 16 c ---[ 103]---> BDD-cost: 11 c ---[ 102]---> BDD-cost: 11 c ---[ 101]---> BDD-cost: 11 c ---[ 100]---> BDD-cost: 11 c ---[ 99]---> BDD-cost: 11 c ---[ 98]---> BDD-cost: 11 c ---[ 97]---> BDD-cost: 11 c ---[ 96]---> BDD-cost: 11 c ---[ 95]---> BDD-cost: 11 c ---[ 94]---> BDD-cost: 11 c ---[ 93]---> BDD-cost: 11 c ---[ 92]---> BDD-cost: 11 c ---[ 91]---> BDD-cost: 11 c ---[ 90]---> BDD-cost: 11 c ---[ 89]---> BDD-cost: 11 c ---[ 88]---> BDD-cost: 11 c ---[ 87]---> BDD-cost: 11 c ---[ 86]---> BDD-cost: 11 c ---[ 85]---> BDD-cost: 11 c ---[ 84]---> BDD-cost: 11 c ---[ 83]---> BDD-cost: 11 c ---[ 82]---> BDD-cost: 11 c ---[ 81]---> BDD-cost: 11 c ---[ 80]---> BDD-cost: 11 c ---[ 79]---> BDD-cost: 11 c ---[ 78]---> BDD-cost: 11 c ---[ 77]---> BDD-cost: 11 c ---[ 76]---> BDD-cost: 11 c ---[ 75]---> BDD-cost: 11 c ---[ 74]---> BDD-cost: 11 c ---[ 73]---> BDD-cost: 11 c ---[ 72]---> BDD-cost: 11 c ---[ 71]---> BDD-cost: 11 c ---[ 70]---> BDD-cost: 11 c ---[ 69]---> BDD-cost: 11 c ---[ 68]---> BDD-cost: 11 c ---[ 67]---> BDD-cost: 11 c ---[ 66]---> BDD-cost: 11 c ---[ 65]---> BDD-cost: 11 c ---[ 64]---> BDD-cost: 11 c ---[ 63]---> BDD-cost: 16 c ---[ 62]---> BDD-cost: 16 c ---[ 61]---> BDD-cost: 16 c ---[ 60]---> BDD-cost: 16 c ---[ 59]---> BDD-cost: 16 c ---[ 58]---> BDD-cost: 16 c ---[ 57]---> BDD-cost: 16 c ---[ 56]---> BDD-cost: 16 c ---[ 55]---> BDD-cost: 16 c ---[ 54]---> BDD-cost: 16 c ---[ 53]---> BDD-cost: 16 c ---[ 52]---> BDD-cost: 16 c ---[ 51]---> BDD-cost: 16 c ---[ 50]---> BDD-cost: 16 c ---[ 49]---> BDD-cost: 16 c ---[ 48]---> BDD-cost: 16 c ---[ 47]---> BDD-cost: 16 c ---[ 46]---> BDD-cost: 16 c ---[ 45]---> BDD-cost: 16 c ---[ 44]---> BDD-cost: 16 c ---[ 42]---> BDD-cost: 282 c ---[ 40]---> BDD-cost: 1158 c ---[ 38]---> BDD-cost: 1158 c ---[ 36]---> BDD-cost: 1158 c ---[ 34]---> BDD-cost: 1158 c ---[ 32]---> BDD-cost: 1158 c ---[ 30]---> BDD-cost: 1158 c ---[ 28]---> BDD-cost: 1158 c ---[ 26]---> BDD-cost: 1158 c ---[ 24]---> BDD-cost: 1158 c ---[ 23]---> BDD-cost: 47 c ---[ 21]---> BDD-cost: 1158 c ---[ 19]---> BDD-cost: 1158 c ---[ 17]---> BDD-cost: 1158 c ---[ 15]---> BDD-cost: 1158 c ---[ 13]---> BDD-cost: 1158 c ---[ 11]---> BDD-cost: 1158 c ---[ 10]---> BDD-cost: 47 c ---[ 9]---> BDD-cost: 47 c ---[ 8]---> BDD-cost: 47 c ---[ 6]---> BDD-cost: 282 c ---[ 4]---> BDD-cost: 282 c ---[ 2]---> BDD-cost: 282 c ---[ 0]---> BDD-cost: 282 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 51929 146608 | 17309 0 0 nan | 0.000 % | c | 101 | 51803 146356 | 19039 95 929 9.8 | 0.701 % | c | 252 | 51803 146356 | 20943 246 3473 14.1 | 0.701 % | c | 478 | 51797 146344 | 23038 470 6416 13.7 | 0.716 % | c | 816 | 51786 146322 | 25342 807 11680 14.5 | 0.743 % | c | 1322 | 51782 146314 | 27876 1311 19267 14.7 | 0.753 % | c | 2081 | 51779 146308 | 30663 2069 41329 20.0 | 0.758 % | c | 3221 | 51779 146308 | 33730 3209 66423 20.7 | 0.758 % | c | 4929 | 51704 146143 | 37103 4901 95170 19.4 | 0.910 % | c | 7491 | 51616 145961 | 40813 7431 151211 20.3 | 1.093 % | c | 11337 | 51616 145961 | 44895 11277 333507 29.6 | 1.093 % | c | 17107 | 51552 145821 | 49384 17006 628732 37.0 | 1.218 % | c | 25757 | 51541 145799 | 54323 25655 872406 34.0 | 1.245 % | c | 38731 | 51522 145760 | 59755 38628 1305809 33.8 | 1.250 % | c | 58192 | 51511 145738 | 65730 58087 1868829 32.2 | 1.276 % | c | 87384 | 51427 145551 | 72303 34293 1556116 45.4 | 1.401 % | c | 131175 | 51333 145357 | 79534 78072 2859918 36.6 | 1.579 % | c | 196861 | 51073 144802 | 87487 78021 2211324 28.3 | 1.951 % | c | 295387 | 50937 144521 | 96236 25221 977684 38.8 | 2.222 % | c | 443176 | 50760 144132 | 105860 90350 4545381 50.3 | 2.473 % | c | 664859 | 50511 143593 | 116446 39851 1295851 32.5 | 2.939 % | c | 997385 | 49929 142324 | 128090 58636 1675081 28.6 | 4.095 % | c ============================================================================== c [1mFound solution: 6092816[0m c ---[ 0]---> Sorter-cost:87749 Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1045219 | 295362 715160 | 98454 106413 2710054 25.5 | 4.095 % | c | 1045320 | 295362 715160 | 108299 14479 316331 21.8 | 0.814 % | c | 1045470 | 295362 715160 | 119129 14629 317171 21.7 | 0.814 % | c | 1045697 | 295362 715160 | 131042 14856 319402 21.5 | 0.814 % | c | 1046035 | 295362 715160 | 144146 15194 322833 21.2 | 0.814 % | c | 1046541 | 295362 715160 | 158561 15700 329947 21.0 | 0.814 % | c | 1047303 | 295331 715095 | 174417 16447 337990 20.6 | 0.829 % | c | 1048442 | 295331 715095 | 191858 17586 362087 20.6 | 0.829 % | c | 1050151 | 295254 714917 | 211044 19193 380991 19.9 | 0.862 % | c | 1052714 | 295254 714917 | 232149 21756 450886 20.7 | 0.862 % | c | 1056558 | 295203 714806 | 255364 25582 511723 20.0 | 0.885 % | c | 1062324 | 295203 714806 | 280900 31348 704532 22.5 | 0.885 % | c | 1070973 | 295169 714731 | 308990 39967 1166896 29.2 | 0.896 % | c | 1083947 | 295169 714731 | 339889 52941 1766041 33.4 | 0.896 % | c c *** TERMINATED *** s SATISFIABLE v -TA1_bit_10 TA1_bit_9 TA1_bit_8 -TA1_bit_7 TA1_bit_6 -TA1_bit_5 TA1_bit_4 TA1_bit_3 TA1_bit_2 -TA1_bit_1 TA1_bit0 -TA1_bit1 TA1_bit2 TA1_bit3 TA1_bit4 TA1_bit5 -TA1_bit6 -TA2_bit_10 TA2_bit_9 -TA2_bit_8 TA2_bit_7 -TA2_bit_6 -TA2_bit_5 -TA2_bit_4 -TA2_bit_3 -TA2_bit_2 TA2_bit_1 TA2_bit0 TA2_bit1 TA2_bit2 TA2_bit3 -TA2_bit4 -TA2_bit5 TA2_bit6 -TA3_bit_10 -TA3_bit_9 -TA3_bit_8 -TA3_bit_7 TA3_bit_6 TA3_bit_5 TA3_bit_4 -TA3_bit_3 TA3_bit_2 TA3_bit_1 TA3_bit0 -TA3_bit1 -TA3_bit2 TA3_bit3 TA3_bit4 TA3_bit5 -TA3_bit6 -TA4_bit_10 -TA4_bit_9 -TA4_bit_8 -TA4_bit_7 TA4_bit_6 TA4_bit_5 TA4_bit_4 TA4_bit_3 TA4_bit_2 -TA4_bit_1 -TA4_bit0 TA4_bit1 -TA4_bit2 -TA4_bit3 TA4_bit4 TA4_bit5 -TA4_bit6 TB1_bit_10 TB1_bit_9 TB1_bit_8 TB1_bit_7 TB1_bit_6 TB1_bit_5 -TB1_bit_4 -TB1_bit_3 -TB1_bit_2 -TB1_bit_1 TB1_bit0 -TB1_bit1 -TB1_bit2 -TB1_bit3 TB1_bit4 TB1_bit5 -TB1_bit6 TB2_bit_10 TB2_bit_9 TB2_bit_8 TB2_bit_7 TB2_bit_6 TB2_bit_5 TB2_bit_4 TB2_bit_3 TB2_bit_2 TB2_bit_1 -TB2_bit0 -TB2_bit1 -TB2_bit2 TB2_bit3 -TB2_bit4 -TB2_bit5 -TB2_bit6 -TB3_bit_10 -TB3_bit_9 -TB3_bit_8 -TB3_bit_7 -TB3_bit_6 -TB3_bit_5 -TB3_bit_4 -TB3_bit_3 -TB3_bit_2 -TB3_bit_1 -TB3_bit0 -TB3_bit1 -TB3_bit2 -TB3_bit3 TB3_bit4 TB3_bit5 -TB3_bit6 -TB4_bit_10 -TB4_bit_9 TB4_bit_8 TB4_bit_7 TB4_bit_6 TB4_bit_5 -TB4_bit_4 -TB4_bit_3 TB4_bit_2 -TB4_bit_1 TB4_bit0 -TB4_bit1 TB4_bit2 -TB4_bit3 TB4_bit4 -TB4_bit5 -TB4_bit6 -TC1_bit_10 TC1_bit_9 -TC1_bit_8 -TC1_bit_7 -TC1_bit_6 -TC1_bit_5 -TC1_bit_4 -TC1_bit_3 -TC1_bit_2 -TC1_bit_1 -TC1_bit0 TC1_bit1 -TC1_bit2 -TC1_bit3 -TC1_bit4 TC1_bit5 -TC1_bit6 TC2_bit_10 TC2_bit_9 TC2_bit_8 -TC2_bit_7 TC2_bit_6 TC2_bit_5 -TC2_bit_4 -TC2_bit_3 -TC2_bit_2 -TC2_bit_1 TC2_bit0 -TC2_bit1 -TC2_bit2 TC2_bit3 TC2_bit4 -TC2_bit5 TC2_bit6 TC3_bit_10 -TC3_bit_9 TC3_bit_8 -TC3_bit_7 -TC3_bit_6 -TC3_bit_5 TC3_bit_4 -TC3_bit_3 TC3_bit_2 -TC3_bit_1 -TC3_bit0 TC3_bit1 -TC3_bit2 -TC3_bit3 -TC3_bit4 TC3_bit5 -TC3_bit6 -TC4_bit_10 -TC4_bit_9 -TC4_bit_8 -TC4_bit_7 -TC4_bit_6 TC4_bit_5 -TC4_bit_4 TC4_bit_3 TC4_bit_2 -TC4_bit_1 -TC4_bit0 TC4_bit1 TC4_bit2 -TC4_bit3 TC4_bit4 TC4_bit5 -TC4_bit6 -TD1_bit_10 -TD1_bit_9 TD1_bit_8 -TD1_bit_7 TD1_bit_6 TD1_bit_5 TD1_bit_4 -TD1_bit_3 TD1_bit_2 TD1_bit_1 -TD1_bit0 TD1_bit1 TD1_bit2 -TD1_bit3 TD1_bit4 -TD1_bit5 TD1_bit6 -TD2_bit_10 -TD2_bit_9 -TD2_bit_8 -TD2_bit_7 -TD2_bit_6 TD2_bit_5 -TD2_bit_4 TD2_bit_3 TD2_bit_2 -TD2_bit_1 -TD2_bit0 -TD2_bit1 -TD2_bit2 -TD2_bit3 -TD2_bit4 -TD2_bit5 TD2_bit6 -TD3_bit_10 -TD3_bit_9 TD3_bit_8 TD3_bit_7 -TD3_bit_6 TD3_bit_5 -TD3_bit_4 -TD3_bit_3 TD3_bit_2 TD3_bit_1 -TD3_bit0 -TD3_bit1 -TD3_bit2 TD3_bit3 -TD3_bit4 -TD3_bit5 -TD3_bit6 -TD4_bit_10 TD4_bit_9 -TD4_bit_8 TD4_bit_7 TD4_bit_6 -TD4_bit_5 TD4_bit_4 -TD4_bit_3 TD4_bit_2 TD4_bit_1 TD4_bit0 -TD4_bit1 TD4_bit2 TD4_bit3 -TD4_bit4 -TD4_bit5 -TD4_bit6 -TE1_bit_10 -TE1_bit_9 -TE1_bit_8 TE1_bit_7 TE1_bit_6 -TE1_bit_5 -TE1_bit_4 -TE1_bit_3 -TE1_bit_2 TE1_bit_1 -TE1_bit0 TE1_bit1 TE1_bit2 TE1_bit3 TE1_bit4 TE1_bit5 -TE1_bit6 -TE2_bit_10 -TE2_bit_9 -TE2_bit_8 -TE2_bit_7 TE2_bit_6 TE2_bit_5 -TE2_bit_4 -TE2_bit_3 -TE2_bit_2 -TE2_bit_1 TE2_bit0 -TE2_bit1 -TE2_bit2 TE2_bit3 TE2_bit4 -TE2_bit5 -TE2_bit6 TE3_bit_10 -TE3_bit_9 TE3_bit_8 TE3_bit_7 -TE3_bit_6 -TE3_bit_5 -TE3_bit_4 -TE3_bit_3 -TE3_bit_2 -TE3_bit_1 TE3_bit0 -TE3_bit1 -TE3_bit2 TE3_bit3 TE3_bit4 -TE3_bit5 -TE3_bit6 TE4_bit_10 -TE4_bit_9 -TE4_bit_8 TE4_bit_7 TE4_bit_6 -TE4_bit_5 -TE4_bit_4 TE4_bit_3 -TE4_bit_2 -TE4_bit_1 TE4_bit0 -TE4_bit1 -TE4_bit2 TE4_bit3 TE4_bit4 -TE4_bit5 -TE4_bit6 -UA1_bit_10 UA1_bit_9 UA1_bit_8 UA1_bit_7 -UA1_bit_6 UA1_bit_5 -UA1_bit_4 -UA1_bit_3 -UA1_bit_2 -UA1_bit_1 UA1_bit0 -UA1_bit1 -UA2_bit_10 -UA2_bit_9 -UA2_bit_8 -UA2_bit_7 -UA2_bit_6 -UA2_bit_5 -UA2_bit_4 -UA2_bit_3 -UA2_bit_2 -UA2_bit_1 -UA2_bit0 UA2_bit1 -UA3_bit_10 -UA3_bit_9 -UA3_bit_8 -UA3_bit_7 UA3_bit_6 UA3_bit_5 -UA3_bit_4 UA3_bit_3 UA3_bit_2 UA3_bit_1 -UA3_bit0 -UA3_bit1 -UA4_bit_10 -UA4_bit_9 -UA4_bit_8 -UA4_bit_7 -UA4_bit_6 UA4_bit_5 UA4_bit_4 UA4_bit_3 UA4_bit_2 -UA4_bit_1 UA4_bit0 -UA4_bit1 UB1_bit_10 -UB1_bit_9 -UB1_bit_8 -UB1_bit_7 -UB1_bit_6 -UB1_bit_5 -UB1_bit_4 -UB1_bit_3 UB1_bit_2 -UB1_bit_1 -UB1_bit0 -UB1_bit1 UB2_bit_10 -UB2_bit_9 -UB2_bit_8 -UB2_bit_7 -UB2_bit_6 -UB2_bit_5 -UB2_bit_4 -UB2_bit_3 -UB2_bit_2 -UB2_bit_1 -UB2_bit0 -UB2_bit1 -UB3_bit_10 -UB3_bit_9 -UB3_bit_8 -UB3_bit_7 -UB3_bit_6 -UB3_bit_5 -UB3_bit_4 -UB3_bit_3 -UB3_bit_2 -UB3_bit_1 -UB3_bit0 -UB3_bit1 -UB4_bit_10 -UB4_bit_9 UB4_bit_8 UB4_bit_7 UB4_bit_6 UB4_bit_5 UB4_bit_4 -UB4_bit_3 -UB4_bit_2 -UB4_bit_1 -UB4_bit0 -UB4_bit1 -UC1_bit_10 -UC1_bit_9 -UC1_bit_8 -UC1_bit_7 -UC1_bit_6 -UC1_bit_5 -UC1_bit_4 -UC1_bit_3 -UC1_bit_2 -UC1_bit_1 -UC1_bit0 -UC1_bit1 UC2_bit_10 -UC2_bit_9 -UC2_bit_8 -UC2_bit_7 -UC2_bit_6 -UC2_bit_5 -UC2_bit_4 -UC2_bit_3 -UC2_bit_2 -UC2_bit_1 UC2_bit0 -UC2_bit1 UC3_bit_10 UC3_bit_9 -UC3_bit_8 -UC3_bit_7 -UC3_bit_6 -UC3_bit_5 -UC3_bit_4 UC3_bit_3 UC3_bit_2 -UC3_bit_1 UC3_bit0 -UC3_bit1 -UC4_bit_10 UC4_bit_9 -UC4_bit_8 UC4_bit_7 -UC4_bit_6 -UC4_bit_5 UC4_bit_4 -UC4_bit_3 -UC4_bit_2 -UC4_bit_1 -UC4_bit0 -UC4_bit1 -UD1_bit_10 -UD1_bit_9 -UD1_bit_8 UD1_bit_7 UD1_bit_6 -UD1_bit_5 -UD1_bit_4 -UD1_bit_3 -UD1_bit_2 -UD1_bit_1 -UD1_bit0 -UD1_bit1 -UD2_bit_10 -UD2_bit_9 -UD2_bit_8 -UD2_bit_7 -UD2_bit_6 -UD2_bit_5 -UD2_bit_4 UD2_bit_3 -UD2_bit_2 UD2_bit_1 -UD2_bit0 -UD2_bit1 -UD3_bit_10 -UD3_bit_9 -UD3_bit_8 -UD3_bit_7 -UD3_bit_6 -UD3_bit_5 -UD3_bit_4 -UD3_bit_3 UD3_bit_2 UD3_bit_1 -UD3_bit0 -UD3_bit1 UD4_bit_10 UD4_bit_9 -UD4_bit_8 UD4_bit_7 UD4_bit_6 UD4_bit_5 UD4_bit_4 UD4_bit_3 -UD4_bit_2 -UD4_bit_1 -UD4_bit0 -UD4_bit1 -UE1_bit_10 -UE1_bit_9 -UE1_bit_8 UE1_bit_7 UE1_bit_6 -UE1_bit_5 -UE1_bit_4 -UE1_bit_3 UE1_bit_2 -UE1_bit_1 UE1_bit0 -UE1_bit1 -UE2_bit_10 -UE2_bit_9 -UE2_bit_8 -UE2_bit_7 -UE2_bit_6 -UE2_bit_5 -UE2_bit_4 -UE2_bit_3 UE2_bit_2 -UE2_bit_1 -UE2_bit0 -UE2_bit1 UE3_bit_10 -UE3_bit_9 -UE3_bit_8 -UE3_bit_7 -UE3_bit_6 -UE3_bit_5 -UE3_bit_4 -UE3_bit_3 -UE3_bit_2 -UE3_bit_1 UE3_bit0 -UE3_bit1 UE4_bit_10 -UE4_bit_9 -UE4_bit_8 UE4_bit_7 UE4_bit_6 UE4_bit_5 UE4_bit_4 UE4_bit_3 -UE4_bit_2 -UE4_bit_1 -UE4_bit0 -UE4_bit1 -VA1_bit_10 -VA1_bit_9 -VA1_bit_8 -VA1_bit_7 -VA1_bit_6 -VA1_bit_5 -VA1_bit_4 -VA1_bit_3 -VA1_bit_2 -VA1_bit_1 -VA1_bit0 VA1_bit1 VA2_bit_10 -VA2_bit_9 VA2_bit_8 VA2_bit_7 VA2_bit_6 VA2_bit_5 VA2_bit_4 VA2_bit_3 -VA2_bit_2 -VA2_bit_1 -VA2_bit0 -VA2_bit1 -VA3_bit_10 -VA3_bit_9 -VA3_bit_8 -VA3_bit_7 -VA3_bit_6 -VA3_bit_5 -VA3_bit_4 -VA3_bit_3 -VA3_bit_2 -VA3_bit_1 -VA3_bit0 VA3_bit1 -VA4_bit_10 VA4_bit_9 -VA4_bit_8 -VA4_bit_7 VA4_bit_6 -VA4_bit_5 -VA4_bit_4 VA4_bit_3 -VA4_bit_2 -VA4_bit_1 -VA4_bit0 -VA4_bit1 -VB1_bit_10 -VB1_bit_9 -VB1_bit_8 -VB1_bit_7 -VB1_bit_6 -VB1_bit_5 -VB1_bit_4 -VB1_bit_3 VB1_bit_2 -VB1_bit_1 -VB1_bit0 -VB1_bit1 -VB2_bit_10 -VB2_bit_9 -VB2_bit_8 -VB2_bit_7 -VB2_bit_6 -VB2_bit_5 -VB2_bit_4 -VB2_bit_3 -VB2_bit_2 -VB2_bit_1 -VB2_bit0 -VB2_bit1 VB3_bit_10 -VB3_bit_9 -VB3_bit_8 -VB3_bit_7 -VB3_bit_6 -VB3_bit_5 -VB3_bit_4 -VB3_bit_3 -VB3_bit_2 -VB3_bit_1 VB3_bit0 -VB3_bit1 VB4_bit_10 VB4_bit_9 VB4_bit_8 VB4_bit_7 -VB4_bit_6 VB4_bit_5 VB4_bit_4 VB4_bit_3 VB4_bit_2 -VB4_bit_1 -VB4_bit0 -VB4_bit1 VC1_bit_10 VC1_bit_9 VC1_bit_8 VC1_bit_7 -VC1_bit_6 VC1_bit_5 -VC1_bit_4 VC1_bit_3 -VC1_bit_2 VC1_bit_1 VC1_bit0 -VC1_bit1 -VC2_bit_10 -VC2_bit_9 -VC2_bit_8 -VC2_bit_7 -VC2_bit_6 VC2_bit_5 VC2_bit_4 -VC2_bit_3 -VC2_bit_2 -VC2_bit_1 -VC2_bit0 -VC2_bit1 -VC3_bit_10 -VC3_bit_9 -VC3_bit_8 -VC3_bit_7 -VC3_bit_6 VC3_bit_5 -VC3_bit_4 VC3_bit_3 -VC3_bit_2 -VC3_bit_1 -VC3_bit0 -VC3_bit1 VC4_bit_10 -VC4_bit_9 VC4_bit_8 VC4_bit_7 -VC4_bit_6 VC4_bit_5 -VC4_bit_4 VC4_bit_3 -VC4_bit_2 VC4_bit_1 VC4_bit0 -VC4_bit1 VD1_bit_10 -VD1_bit_9 VD1_bit_8 -VD1_bit_7 -VD1_bit_6 -VD1_bit_5 VD1_bit_4 -VD1_bit_3 VD1_bit_2 -VD1_bit_1 -VD1_bit0 -VD1_bit1 -VD2_bit_10 -VD2_bit_9 -VD2_bit_8 VD2_bit_7 -VD2_bit_6 -VD2_bit_5 -VD2_bit_4 -VD2_bit_3 -VD2_bit_2 -VD2_bit_1 -VD2_bit0 -VD2_bit1 -VD3_bit_10 VD3_bit_9 VD3_bit_8 VD3_bit_7 VD3_bit_6 -VD3_bit_5 -VD3_bit_4 -VD3_bit_3 -VD3_bit_2 -VD3_bit_1 -VD3_bit0 -VD3_bit1 -VD4_bit_10 -VD4_bit_9 -VD4_bit_8 -VD4_bit_7 -VD4_bit_6 -VD4_bit_5 -VD4_bit_4 -VD4_bit_3 -VD4_bit_2 -VD4_bit_1 -VD4_bit0 VD4_bit1 -VE1_bit_10 -VE1_bit_9 -VE1_bit_8 -VE1_bit_7 VE1_bit_6 -VE1_bit_5 -VE1_bit_4 VE1_bit_3 -VE1_bit_2 VE1_bit_1 -VE1_bit0 -VE1_bit1 -VE2_bit_10 -VE2_bit_9 -VE2_bit_8 -VE2_bit_7 -VE2_bit_6 -VE2_bit_5 -VE2_bit_4 VE2_bit_3 -VE2_bit_2 -VE2_bit_1 -VE2_bit0 -VE2_bit1 -VE3_bit_10 -VE3_bit_9 -VE3_bit_8 -VE3_bit_7 -VE3_bit_6 VE3_bit_5 -VE3_bit_4 -VE3_bit_3 VE3_bit_2 -VE3_bit_1 -VE3_bit0 -VE3_bit1 -VE4_bit_10 -VE4_bit_9 -VE4_bit_8 -VE4_bit_7 -VE4_bit_6 -VE4_bit_5 -VE4_bit_4 -VE4_bit_3 -VE4_bit_2 -VE4_bit_1 -VE4_bit0 -VE4_bit1 -WA1_bit_10 -WA1_bit_9 WA1_bit_8 -WA1_bit_7 -WA1_bit_6 -WA1_bit_5 -WA1_bit_4 -WA1_bit_3 -WA1_bit_2 -WA1_bit_1 -WA1_bit0 -WA1_bit1 -WA1_bit2 -WA1_bit3 -WA1_bit4 -WA1_bit5 WA1_bit6 WA2_bit_10 -WA2_bit_9 WA2_bit_8 WA2_bit_7 -WA2_bit_6 -WA2_bit_5 -WA2_bit_4 -WA2_bit_3 WA2_bit_2 -WA2_bit_1 -WA2_bit0 -WA2_bit1 -WA2_bit2 WA2_bit3 WA2_bit4 -WA2_bit5 WA2_bit6 -WA3_bit_10 -WA3_bit_9 -WA3_bit_8 -WA3_bit_7 -WA3_bit_6 WA3_bit_5 -WA3_bit_4 -WA3_bit_3 WA3_bit_2 -WA3_bit_1 WA3_bit0 WA3_bit1 -WA3_bit2 -WA3_bit3 -WA3_bit4 -WA3_bit5 WA3_bit6 -WA4_bit_10 WA4_bit_9 WA4_bit_8 WA4_bit_7 WA4_bit_6 WA4_bit_5 -WA4_bit_4 -WA4_bit_3 WA4_bit_2 WA4_bit_1 WA4_bit0 -WA4_bit1 -WA4_bit2 -WA4_bit3 -WA4_bit4 -WA4_bit5 WA4_bit6 -WB1_bit_10 -WB1_bit_9 -WB1_bit_8 -WB1_bit_7 -WB1_bit_6 -WB1_bit_5 WB1_bit_4 -WB1_bit_3 -WB1_bit_2 WB1_bit_1 -WB1_bit0 -WB1_bit1 WB1_bit2 -WB1_bit3 WB1_bit4 WB1_bit5 -WB1_bit6 -WB2_bit_10 -WB2_bit_9 -WB2_bit_8 -WB2_bit_7 -WB2_bit_6 -WB2_bit_5 -WB2_bit_4 -WB2_bit_3 -WB2_bit_2 -WB2_bit_1 -WB2_bit0 -WB2_bit1 -WB2_bit2 -WB2_bit3 WB2_bit4 -WB2_bit5 -WB2_bit6 WB3_bit_10 WB3_bit_9 WB3_bit_8 WB3_bit_7 WB3_bit_6 WB3_bit_5 WB3_bit_4 WB3_bit_3 WB3_bit_2 -WB3_bit_1 WB3_bit0 -WB3_bit1 -WB3_bit2 WB3_bit3 WB3_bit4 WB3_bit5 -WB3_bit6 WB4_bit_10 -WB4_bit_9 -WB4_bit_8 WB4_bit_7 -WB4_bit_6 -WB4_bit_5 WB4_bit_4 WB4_bit_3 WB4_bit_2 WB4_bit_1 -WB4_bit0 WB4_bit1 -WB4_bit2 -WB4_bit3 -WB4_bit4 WB4_bit5 -WB4_bit6 WC1_bit_10 WC1_bit_9 -WC1_bit_8 -WC1_bit_7 WC1_bit_6 -WC1_bit_5 WC1_bit_4 -WC1_bit_3 WC1_bit_2 WC1_bit_1 WC1_bit0 WC1_bit1 -WC1_bit2 -WC1_bit3 -WC1_bit4 WC1_bit5 -WC1_bit6 -WC2_bit_10 -WC2_bit_9 -WC2_bit_8 WC2_bit_7 WC2_bit_6 -WC2_bit_5 WC2_bit_4 WC2_bit_3 WC2_bit_2 WC2_bit_1 -WC2_bit0 -WC2_bit1 -WC2_bit2 -WC2_bit3 -WC2_bit4 WC2_bit5 WC2_bit6 -WC3_bit_10 -WC3_bit_9 -WC3_bit_8 WC3_bit_7 -WC3_bit_6 WC3_bit_5 -WC3_bit_4 -WC3_bit_3 -WC3_bit_2 -WC3_bit_1 -WC3_bit0 WC3_bit1 WC3_bit2 WC3_bit3 -WC3_bit4 WC3_bit5 -WC3_bit6 WC4_bit_10 -WC4_bit_9 WC4_bit_8 WC4_bit_7 WC4_bit_6 WC4_bit_5 -WC4_bit_4 -WC4_bit_3 WC4_bit_2 WC4_bit_1 -WC4_bit0 WC4_bit1 -WC4_bit2 -WC4_bit3 -WC4_bit4 -WC4_bit5 WC4_bit6 WD1_bit_10 WD1_bit_9 WD1_bit_8 -WD1_bit_7 -WD1_bit_6 -WD1_bit_5 WD1_bit_4 -WD1_bit_3 -WD1_bit_2 -WD1_bit_1 -WD1_bit0 WD1_bit1 -WD1_bit2 WD1_bit3 WD1_bit4 -WD1_bit5 WD1_bit6 -WD2_bit_10 -WD2_bit_9 -WD2_bit_8 WD2_bit_7 WD2_bit_6 -WD2_bit_5 -WD2_bit_4 -WD2_bit_3 -WD2_bit_2 -WD2_bit_1 -WD2_bit0 -WD2_bit1 -WD2_bit2 WD2_bit3 -WD2_bit4 -WD2_bit5 WD2_bit6 -WD3_bit_10 WD3_bit_9 WD3_bit_8 WD3_bit_7 -WD3_bit_6 -WD3_bit_5 -WD3_bit_4 -WD3_bit_3 -WD3_bit_2 -WD3_bit_1 -WD3_bit0 -WD3_bit1 WD3_bit2 -WD3_bit3 WD3_bit4 -WD3_bit5 -WD3_bit6 WD4_bit_10 -WD4_bit_9 WD4_bit_8 -WD4_bit_7 WD4_bit_6 -WD4_bit_5 WD4_bit_4 -WD4_bit_3 -WD4_bit_2 -WD4_bit_1 -WD4_bit0 WD4_bit1 -WD4_bit2 WD4_bit3 WD4_bit4 -WD4_bit5 -WD4_bit6 -WE1_bit_10 -WE1_bit_9 -WE1_bit_8 -WE1_bit_7 -WE1_bit_6 WE1_bit_5 -WE1_bit_4 WE1_bit_3 -WE1_bit_2 WE1_bit_1 -WE1_bit0 WE1_bit1 -WE1_bit2 -WE1_bit3 -WE1_bit4 -WE1_bit5 WE1_bit6 -WE2_bit_10 -WE2_bit_9 -WE2_bit_8 -WE2_bit_7 WE2_bit_6 WE2_bit_5 -WE2_bit_4 WE2_bit_3 -WE2_bit_2 -WE2_bit_1 -WE2_bit0 -WE2_bit1 -WE2_bit2 -WE2_bit3 -WE2_bit4 WE2_bit5 -WE2_bit6 -WE3_bit_10 WE3_bit_9 WE3_bit_8 WE3_bit_7 -WE3_bit_6 WE3_bit_5 WE3_bit_4 WE3_bit_3 -WE3_bit_2 -WE3_bit_1 -WE3_bit0 -WE3_bit1 WE3_bit2 -WE3_bit3 -WE3_bit4 WE3_bit5 -WE3_bit6 -WE4_bit_10 WE4_bit_9 -WE4_bit_8 -WE4_bit_7 WE4_bit_6 -WE4_bit_5 -WE4_bit_4 WE4_bit_3 WE4_bit_2 -WE4_bit_1 WE4_bit0 WE4_bit1 WE4_bit2 -WE4_bit3 -WE4_bit4 WE4_bit5 -WE4_bit6 -A1_bit0 -B1_bit0 -C1_bit0 -D1_bit0 -E1_bit0 -AB1_bit0 -AC1_bit0 -AD1_bit0 -AE1_bit0 -BC1_bit0 -BD1_bit0 -BE1_bit0 -CD1_bit0 -CE1_bit0 -DE1_bit0 -ABC1_bit0 -ABD1_b
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/23047/stat): 23047 (minisat+_script) R 23046 23047 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851937187 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/23047/statm): 174 3 169 147 0 27 0 [pid=23047] 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=23048 New process pid=23049 New process pid=23050 One traced child (pid=23049) exited with status: 0 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 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=23050) exited with status: 0 One traced child (pid=23048) exited with status: 0 New process pid=23051 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-rgn.opb [startup+10.0038 s] Raw data (loadavg): 0.82 0.93 0.88 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 3284 0 0 0 966 14 0 0 22 0 1 0 1851937192 12279808 2676 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 2998 2676 145 145 0 2853 0 [pid=23051] vsize: 11992 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 14116 [startup+20.0056 s] Raw data (loadavg): 0.85 0.93 0.88 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 4189 0 0 0 1954 19 0 0 25 0 1 0 1851937192 16060416 3581 4294967295 134512640 135094434 3221224432 3221223104 134556166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 3921 3581 145 145 0 3776 0 [pid=23051] vsize: 15684 Current children cumulated CPU time (s) 19.73 Current children cumulated vsize (Kb) 17808 [startup+30.0073 s] Raw data (loadavg): 0.87 0.93 0.88 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 4843 0 0 0 2943 24 0 0 25 0 1 0 1851937192 18694144 4235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 4564 4235 145 145 0 4419 0 [pid=23051] vsize: 18256 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 20380 [startup+40.008 s] Raw data (loadavg): 0.89 0.93 0.88 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5425 0 0 0 3935 28 0 0 25 0 1 0 1851937192 21331968 4817 4294967295 134512640 135094434 3221224432 3221223184 134559163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 5208 4817 145 145 0 5063 0 [pid=23051] vsize: 20832 Current children cumulated CPU time (s) 39.63 Current children cumulated vsize (Kb) 22956 [startup+50.0097 s] Raw data (loadavg): 0.91 0.93 0.88 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5426 0 0 0 4935 28 0 0 25 0 1 0 1851937192 21331968 4818 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 5208 4818 145 145 0 5063 0 [pid=23051] vsize: 20832 Current children cumulated CPU time (s) 49.63 Current children cumulated vsize (Kb) 22956 [startup+60.0104 s] Raw data (loadavg): 0.92 0.94 0.88 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5462 0 0 0 5934 29 0 0 25 0 1 0 1851937192 21528576 4854 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 5256 4854 145 145 0 5111 0 [pid=23051] vsize: 21024 Current children cumulated CPU time (s) 59.63 Current children cumulated vsize (Kb) 23148 [startup+70.0122 s] Raw data (loadavg): 0.93 0.94 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 5681 0 0 0 6930 30 0 0 25 0 1 0 1851937192 22433792 5073 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 5477 5073 145 145 0 5332 0 [pid=23051] vsize: 21908 Current children cumulated CPU time (s) 69.6 Current children cumulated vsize (Kb) 24032 [startup+80.0129 s] Raw data (loadavg): 0.94 0.94 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6329 0 0 0 7920 34 0 0 25 0 1 0 1851937192 25079808 5721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6123 5721 145 145 0 5978 0 [pid=23051] vsize: 24492 Current children cumulated CPU time (s) 79.54 Current children cumulated vsize (Kb) 26616 [startup+90.0136 s] Raw data (loadavg): 0.95 0.94 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6376 0 0 0 8919 35 0 0 25 0 1 0 1851937192 25264128 5768 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6168 5768 145 145 0 6023 0 [pid=23051] vsize: 24672 Current children cumulated CPU time (s) 89.54 Current children cumulated vsize (Kb) 26796 [startup+100.015 s] Raw data (loadavg): 0.96 0.94 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6376 0 0 0 9918 36 0 0 25 0 1 0 1851937192 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6168 5768 145 145 0 6023 0 [pid=23051] vsize: 24672 Current children cumulated CPU time (s) 99.54 Current children cumulated vsize (Kb) 26796 [startup+110.016 s] Raw data (loadavg): 0.96 0.94 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6376 0 0 0 10918 36 0 0 25 0 1 0 1851937192 25264128 5768 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6168 5768 145 145 0 6023 0 [pid=23051] vsize: 24672 Current children cumulated CPU time (s) 109.54 Current children cumulated vsize (Kb) 26796 [startup+120.018 s] Raw data (loadavg): 0.97 0.94 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6390 0 0 0 11917 37 0 0 25 0 1 0 1851937192 25329664 5782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6184 5782 145 145 0 6039 0 [pid=23051] vsize: 24736 Current children cumulated CPU time (s) 119.54 Current children cumulated vsize (Kb) 26860 [startup+130.019 s] Raw data (loadavg): 0.97 0.95 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6426 0 0 0 12916 38 0 0 25 0 1 0 1851937192 25493504 5818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6224 5818 145 145 0 6079 0 [pid=23051] vsize: 24896 Current children cumulated CPU time (s) 129.54 Current children cumulated vsize (Kb) 27020 [startup+140.019 s] Raw data (loadavg): 0.98 0.95 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6432 0 0 0 13916 38 0 0 25 0 1 0 1851937192 25493504 5824 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6224 5824 145 145 0 6079 0 [pid=23051] vsize: 24896 Current children cumulated CPU time (s) 139.54 Current children cumulated vsize (Kb) 27020 [startup+150.021 s] Raw data (loadavg): 0.98 0.95 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6432 0 0 0 14915 39 0 0 25 0 1 0 1851937192 25493504 5824 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6224 5824 145 145 0 6079 0 [pid=23051] vsize: 24896 Current children cumulated CPU time (s) 149.54 Current children cumulated vsize (Kb) 27020 [startup+160.022 s] Raw data (loadavg): 0.98 0.95 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6447 0 0 0 15915 39 0 0 25 0 1 0 1851937192 25591808 5839 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6248 5839 145 145 0 6103 0 [pid=23051] vsize: 24992 Current children cumulated CPU time (s) 159.54 Current children cumulated vsize (Kb) 27116 [startup+170.022 s] Raw data (loadavg): 0.98 0.95 0.89 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6460 0 0 0 16914 40 0 0 25 0 1 0 1851937192 25657344 5852 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6264 5852 145 145 0 6119 0 [pid=23051] vsize: 25056 Current children cumulated CPU time (s) 169.54 Current children cumulated vsize (Kb) 27180 [startup+180.023 s] Raw data (loadavg): 0.99 0.95 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6750 0 0 0 17909 42 0 0 25 0 1 0 1851937192 26869760 6142 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6560 6142 145 145 0 6415 0 [pid=23051] vsize: 26240 Current children cumulated CPU time (s) 179.51 Current children cumulated vsize (Kb) 28364 [startup+190.024 s] Raw data (loadavg): 0.99 0.95 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6957 0 0 0 18907 43 0 0 25 0 1 0 1851937192 27783168 6349 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 6783 6349 145 145 0 6638 0 [pid=23051] vsize: 27132 Current children cumulated CPU time (s) 189.5 Current children cumulated vsize (Kb) 29256 [startup+200.025 s] Raw data (loadavg): 0.99 0.95 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6959 0 0 0 19907 43 0 0 25 0 1 0 1851937192 27783168 6351 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 6783 6351 145 145 0 6638 0 [pid=23051] vsize: 27132 Current children cumulated CPU time (s) 199.5 Current children cumulated vsize (Kb) 29256 [startup+210.025 s] Raw data (loadavg): 0.99 0.95 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 6968 0 0 0 20907 43 0 0 25 0 1 0 1851937192 27832320 6360 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 6795 6360 145 145 0 6650 0 [pid=23051] vsize: 27180 Current children cumulated CPU time (s) 209.5 Current children cumulated vsize (Kb) 29304 [startup+220.027 s] Raw data (loadavg): 0.99 0.95 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7017 0 0 0 21907 43 0 0 25 0 1 0 1851937192 28061696 6409 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 6851 6409 145 145 0 6706 0 [pid=23051] vsize: 27404 Current children cumulated CPU time (s) 219.5 Current children cumulated vsize (Kb) 29528 [startup+230.028 s] Raw data (loadavg): 0.99 0.95 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7065 0 0 0 22906 43 0 0 25 0 1 0 1851937192 28258304 6457 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 6899 6457 145 145 0 6754 0 [pid=23051] vsize: 27596 Current children cumulated CPU time (s) 229.49 Current children cumulated vsize (Kb) 29720 [startup+240.029 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7174 0 0 0 23906 44 0 0 25 0 1 0 1851937192 28790784 6566 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7029 6566 145 145 0 6884 0 [pid=23051] vsize: 28116 Current children cumulated CPU time (s) 239.5 Current children cumulated vsize (Kb) 30240 [startup+250.029 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7395 0 0 0 24902 45 0 0 25 0 1 0 1851937192 29704192 6787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7252 6787 145 145 0 7107 0 [pid=23051] vsize: 29008 Current children cumulated CPU time (s) 249.47 Current children cumulated vsize (Kb) 31132 [startup+260.03 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7646 0 0 0 25898 47 0 0 25 0 1 0 1851937192 30732288 7038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7503 7038 145 145 0 7358 0 [pid=23051] vsize: 30012 Current children cumulated CPU time (s) 259.45 Current children cumulated vsize (Kb) 32136 [startup+270.031 s] Raw data (loadavg): 0.99 0.96 0.90 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 26895 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0 [pid=23051] vsize: 30740 Current children cumulated CPU time (s) 269.44 Current children cumulated vsize (Kb) 32864 [startup+280.031 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 27895 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0 [pid=23051] vsize: 30740 Current children cumulated CPU time (s) 279.44 Current children cumulated vsize (Kb) 32864 [startup+290.032 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 28895 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0 [pid=23051] vsize: 30740 Current children cumulated CPU time (s) 289.44 Current children cumulated vsize (Kb) 32864 [startup+300.033 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 29896 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0 [pid=23051] vsize: 30740 Current children cumulated CPU time (s) 299.45 Current children cumulated vsize (Kb) 32864 [startup+310.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 7824 0 0 0 30896 49 0 0 25 0 1 0 1851937192 31477760 7216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 7685 7216 145 145 0 7540 0 [pid=23051] vsize: 30740 Current children cumulated CPU time (s) 309.45 Current children cumulated vsize (Kb) 32864 [startup+320.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 8236 0 0 0 31890 51 0 0 25 0 1 0 1851937192 33218560 7628 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 8110 7628 145 145 0 7965 0 [pid=23051] vsize: 32440 Current children cumulated CPU time (s) 319.41 Current children cumulated vsize (Kb) 34564 [startup+330.035 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 8616 0 0 0 32884 54 0 0 25 0 1 0 1851937192 34893824 8008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 8519 8008 145 145 0 8374 0 [pid=23051] vsize: 34076 Current children cumulated CPU time (s) 329.38 Current children cumulated vsize (Kb) 36200 [startup+340.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 8893 0 0 0 33881 55 0 0 25 0 1 0 1851937192 36110336 8285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 8816 8285 145 145 0 8671 0 [pid=23051] vsize: 35264 Current children cumulated CPU time (s) 339.36 Current children cumulated vsize (Kb) 37388 [startup+350.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 9203 0 0 0 34876 58 0 0 25 0 1 0 1851937192 37462016 8595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 9146 8595 145 145 0 9001 0 [pid=23051] vsize: 36584 Current children cumulated CPU time (s) 349.34 Current children cumulated vsize (Kb) 38708 [startup+360.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 9477 0 0 0 35871 60 0 0 25 0 1 0 1851937192 38645760 8869 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 9435 8869 145 145 0 9290 0 [pid=23051] vsize: 37740 Current children cumulated CPU time (s) 359.31 Current children cumulated vsize (Kb) 39864 [startup+370.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 9757 0 0 0 36867 62 0 0 25 0 1 0 1851937192 39817216 9149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 9721 9149 145 145 0 9576 0 [pid=23051] vsize: 38884 Current children cumulated CPU time (s) 369.29 Current children cumulated vsize (Kb) 41008 [startup+380.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10195 0 0 0 37860 64 0 0 25 0 1 0 1851937192 41603072 9587 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10157 9587 145 145 0 10012 0 [pid=23051] vsize: 40628 Current children cumulated CPU time (s) 379.24 Current children cumulated vsize (Kb) 42752 [startup+390.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10195 0 0 0 38861 64 0 0 25 0 1 0 1851937192 41603072 9587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10157 9587 145 145 0 10012 0 [pid=23051] vsize: 40628 Current children cumulated CPU time (s) 389.25 Current children cumulated vsize (Kb) 42752 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10196 0 0 0 39860 64 0 0 25 0 1 0 1851937192 41603072 9588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10157 9588 145 145 0 10012 0 [pid=23051] vsize: 40628 Current children cumulated CPU time (s) 399.24 Current children cumulated vsize (Kb) 42752 [startup+410.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10196 0 0 0 40861 64 0 0 25 0 1 0 1851937192 41603072 9588 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10157 9588 145 145 0 10012 0 [pid=23051] vsize: 40628 Current children cumulated CPU time (s) 409.25 Current children cumulated vsize (Kb) 42752 [startup+420.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10219 0 0 0 41861 64 0 0 25 0 1 0 1851937192 41734144 9611 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10189 9611 145 145 0 10044 0 [pid=23051] vsize: 40756 Current children cumulated CPU time (s) 419.25 Current children cumulated vsize (Kb) 42880 [startup+430.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10220 0 0 0 42861 64 0 0 25 0 1 0 1851937192 41734144 9612 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10189 9612 145 145 0 10044 0 [pid=23051] vsize: 40756 Current children cumulated CPU time (s) 429.25 Current children cumulated vsize (Kb) 42880 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10240 0 0 0 43861 64 0 0 25 0 1 0 1851937192 41865216 9632 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10221 9632 145 145 0 10076 0 [pid=23051] vsize: 40884 Current children cumulated CPU time (s) 439.25 Current children cumulated vsize (Kb) 43008 [startup+450.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10242 0 0 0 44862 64 0 0 25 0 1 0 1851937192 41865216 9634 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10221 9634 145 145 0 10076 0 [pid=23051] vsize: 40884 Current children cumulated CPU time (s) 449.26 Current children cumulated vsize (Kb) 43008 [startup+460.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10264 0 0 0 45861 65 0 0 25 0 1 0 1851937192 41996288 9656 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10253 9656 145 145 0 10108 0 [pid=23051] vsize: 41012 Current children cumulated CPU time (s) 459.26 Current children cumulated vsize (Kb) 43136 [startup+470.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10306 0 0 0 46861 65 0 0 25 0 1 0 1851937192 42258432 9698 4294967295 134512640 135094434 3221224432 3221223088 134558144 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10317 9698 145 145 0 10172 0 [pid=23051] vsize: 41268 Current children cumulated CPU time (s) 469.26 Current children cumulated vsize (Kb) 43392 [startup+480.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10328 0 0 0 47862 65 0 0 25 0 1 0 1851937192 42389504 9720 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10349 9720 145 145 0 10204 0 [pid=23051] vsize: 41396 Current children cumulated CPU time (s) 479.27 Current children cumulated vsize (Kb) 43520 [startup+490.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10334 0 0 0 48862 65 0 0 25 0 1 0 1851937192 42389504 9726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10349 9726 145 145 0 10204 0 [pid=23051] vsize: 41396 Current children cumulated CPU time (s) 489.27 Current children cumulated vsize (Kb) 43520 [startup+500.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10362 0 0 0 49862 65 0 0 25 0 1 0 1851937192 42520576 9754 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10381 9754 145 145 0 10236 0 [pid=23051] vsize: 41524 Current children cumulated CPU time (s) 499.27 Current children cumulated vsize (Kb) 43648 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10385 0 0 0 50862 65 0 0 25 0 1 0 1851937192 42651648 9777 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10413 9777 145 145 0 10268 0 [pid=23051] vsize: 41652 Current children cumulated CPU time (s) 509.27 Current children cumulated vsize (Kb) 43776 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10410 0 0 0 51862 65 0 0 25 0 1 0 1851937192 42782720 9802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10445 9802 145 145 0 10300 0 [pid=23051] vsize: 41780 Current children cumulated CPU time (s) 519.27 Current children cumulated vsize (Kb) 43904 [startup+530.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10430 0 0 0 52862 66 0 0 25 0 1 0 1851937192 42913792 9822 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9822 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 529.28 Current children cumulated vsize (Kb) 44032 [startup+540.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 53862 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 539.28 Current children cumulated vsize (Kb) 44032 [startup+550.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 54863 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 549.29 Current children cumulated vsize (Kb) 44032 [startup+560.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 55863 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 559.29 Current children cumulated vsize (Kb) 44032 [startup+570.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10433 0 0 0 56863 66 0 0 25 0 1 0 1851937192 42913792 9825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9825 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 569.29 Current children cumulated vsize (Kb) 44032 [startup+580.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 57863 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 579.29 Current children cumulated vsize (Kb) 44032 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 58864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 589.3 Current children cumulated vsize (Kb) 44032 [startup+600.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 59864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 599.3 Current children cumulated vsize (Kb) 44032 [startup+610.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 60864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 609.3 Current children cumulated vsize (Kb) 44032 [startup+620.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 61864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 619.3 Current children cumulated vsize (Kb) 44032 [startup+630.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 62864 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 629.3 Current children cumulated vsize (Kb) 44032 [startup+640.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 63865 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 639.31 Current children cumulated vsize (Kb) 44032 [startup+650.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 64865 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 649.31 Current children cumulated vsize (Kb) 44032 [startup+660.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10437 0 0 0 65865 66 0 0 25 0 1 0 1851937192 42913792 9829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10477 9829 145 145 0 10332 0 [pid=23051] vsize: 41908 Current children cumulated CPU time (s) 659.31 Current children cumulated vsize (Kb) 44032 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10471 0 0 0 66865 66 0 0 25 0 1 0 1851937192 43175936 9863 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10541 9863 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 669.31 Current children cumulated vsize (Kb) 44288 [startup+680.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 67866 66 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 679.32 Current children cumulated vsize (Kb) 44288 [startup+690.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 68866 67 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 689.33 Current children cumulated vsize (Kb) 44288 [startup+700.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 69865 67 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 699.32 Current children cumulated vsize (Kb) 44288 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 70864 67 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 709.31 Current children cumulated vsize (Kb) 44288 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 71863 68 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 719.31 Current children cumulated vsize (Kb) 44288 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10473 0 0 0 72863 69 0 0 25 0 1 0 1851937192 43175936 9865 4294967295 134512640 135094434 3221224432 3221223104 134555795 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10541 9865 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 729.32 Current children cumulated vsize (Kb) 44288 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10476 0 0 0 73863 69 0 0 25 0 1 0 1851937192 43175936 9868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10541 9868 145 145 0 10396 0 [pid=23051] vsize: 42164 Current children cumulated CPU time (s) 739.32 Current children cumulated vsize (Kb) 44288 [startup+750.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10683 0 0 0 74860 71 0 0 25 0 1 0 1851937192 44027904 10075 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10749 10075 145 145 0 10604 0 [pid=23051] vsize: 42996 Current children cumulated CPU time (s) 749.31 Current children cumulated vsize (Kb) 45120 [startup+760.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10800 0 0 0 75858 71 0 0 25 0 1 0 1851937192 44498944 10192 4294967295 134512640 135094434 3221224432 3221223088 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10864 10192 145 145 0 10719 0 [pid=23051] vsize: 43456 Current children cumulated CPU time (s) 759.29 Current children cumulated vsize (Kb) 45580 [startup+770.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10826 0 0 0 76858 72 0 0 25 0 1 0 1851937192 44630016 10218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10896 10218 145 145 0 10751 0 [pid=23051] vsize: 43584 Current children cumulated CPU time (s) 769.3 Current children cumulated vsize (Kb) 45708 [startup+780.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10835 0 0 0 77858 72 0 0 25 0 1 0 1851937192 44756992 10227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10927 10227 145 145 0 10782 0 [pid=23051] vsize: 43708 Current children cumulated CPU time (s) 779.3 Current children cumulated vsize (Kb) 45832 [startup+790.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10855 0 0 0 78858 72 0 0 25 0 1 0 1851937192 44822528 10247 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 10943 10247 145 145 0 10798 0 [pid=23051] vsize: 43772 Current children cumulated CPU time (s) 789.3 Current children cumulated vsize (Kb) 45896 [startup+800.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10906 0 0 0 79858 73 0 0 25 0 1 0 1851937192 45215744 10298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11039 10298 145 145 0 10894 0 [pid=23051] vsize: 44156 Current children cumulated CPU time (s) 799.31 Current children cumulated vsize (Kb) 46280 [startup+810.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 10988 0 0 0 80857 73 0 0 25 0 1 0 1851937192 45674496 10380 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11151 10380 145 145 0 11006 0 [pid=23051] vsize: 44604 Current children cumulated CPU time (s) 809.3 Current children cumulated vsize (Kb) 46728 [startup+820.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11015 0 0 0 81857 73 0 0 25 0 1 0 1851937192 45740032 10407 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11167 10407 145 145 0 11022 0 [pid=23051] vsize: 44668 Current children cumulated CPU time (s) 819.3 Current children cumulated vsize (Kb) 46792 [startup+830.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11021 0 0 0 82857 74 0 0 25 0 1 0 1851937192 45740032 10413 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11167 10413 145 145 0 11022 0 [pid=23051] vsize: 44668 Current children cumulated CPU time (s) 829.31 Current children cumulated vsize (Kb) 46792 [startup+840.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11040 0 0 0 83857 74 0 0 25 0 1 0 1851937192 45805568 10432 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11183 10432 145 145 0 11038 0 [pid=23051] vsize: 44732 Current children cumulated CPU time (s) 839.31 Current children cumulated vsize (Kb) 46856 [startup+850.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11104 0 0 0 84857 74 0 0 25 0 1 0 1851937192 46084096 10496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11251 10496 145 145 0 11106 0 [pid=23051] vsize: 45004 Current children cumulated CPU time (s) 849.31 Current children cumulated vsize (Kb) 47128 [startup+860.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11365 0 0 0 85853 76 0 0 25 0 1 0 1851937192 47140864 10757 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11509 10757 145 145 0 11364 0 [pid=23051] vsize: 46036 Current children cumulated CPU time (s) 859.29 Current children cumulated vsize (Kb) 48160 [startup+870.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11588 0 0 0 86849 78 0 0 25 0 1 0 1851937192 48111616 10980 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11746 10980 145 145 0 11601 0 [pid=23051] vsize: 46984 Current children cumulated CPU time (s) 869.27 Current children cumulated vsize (Kb) 49108 [startup+880.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 11810 0 0 0 87846 79 0 0 25 0 1 0 1851937192 48967680 11202 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 11955 11202 145 145 0 11810 0 [pid=23051] vsize: 47820 Current children cumulated CPU time (s) 879.25 Current children cumulated vsize (Kb) 49944 [startup+890.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12009 0 0 0 88843 81 0 0 25 0 1 0 1851937192 49774592 11401 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 12152 11401 145 145 0 12007 0 [pid=23051] vsize: 48608 Current children cumulated CPU time (s) 889.24 Current children cumulated vsize (Kb) 50732 [startup+900.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12254 0 0 0 89839 82 0 0 25 0 1 0 1851937192 50982912 11646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 12447 11646 145 145 0 12302 0 [pid=23051] vsize: 49788 Current children cumulated CPU time (s) 899.21 Current children cumulated vsize (Kb) 51912 [startup+910.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12475 0 0 0 90836 84 0 0 25 0 1 0 1851937192 51879936 11867 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 12666 11867 145 145 0 12521 0 [pid=23051] vsize: 50664 Current children cumulated CPU time (s) 909.2 Current children cumulated vsize (Kb) 52788 [startup+920.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12657 0 0 0 91834 85 0 0 25 0 1 0 1851937192 52744192 12049 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 12877 12049 145 145 0 12732 0 [pid=23051] vsize: 51508 Current children cumulated CPU time (s) 919.19 Current children cumulated vsize (Kb) 53632 [startup+930.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 12835 0 0 0 92831 86 0 0 25 0 1 0 1851937192 53465088 12227 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13053 12227 145 145 0 12908 0 [pid=23051] vsize: 52212 Current children cumulated CPU time (s) 929.17 Current children cumulated vsize (Kb) 54336 [startup+940.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13015 0 0 0 93828 88 0 0 25 0 1 0 1851937192 54198272 12407 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13232 12407 145 145 0 13087 0 [pid=23051] vsize: 52928 Current children cumulated CPU time (s) 939.16 Current children cumulated vsize (Kb) 55052 [startup+950.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13197 0 0 0 94825 89 0 0 25 0 1 0 1851937192 54951936 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13416 12589 145 145 0 13271 0 [pid=23051] vsize: 53664 Current children cumulated CPU time (s) 949.14 Current children cumulated vsize (Kb) 55788 [startup+960.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 95825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 959.14 Current children cumulated vsize (Kb) 56128 [startup+970.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 96825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 969.14 Current children cumulated vsize (Kb) 56128 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 97825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 979.14 Current children cumulated vsize (Kb) 56128 [startup+990.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 98826 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 989.15 Current children cumulated vsize (Kb) 56128 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 99825 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 999.14 Current children cumulated vsize (Kb) 56128 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 100826 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 1009.15 Current children cumulated vsize (Kb) 56128 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13283 0 0 0 101826 89 0 0 25 0 1 0 1851937192 55300096 12675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13501 12675 145 145 0 13356 0 [pid=23051] vsize: 54004 Current children cumulated CPU time (s) 1019.15 Current children cumulated vsize (Kb) 56128 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 102826 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0 [pid=23051] vsize: 54100 Current children cumulated CPU time (s) 1029.16 Current children cumulated vsize (Kb) 56224 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 103826 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0 [pid=23051] vsize: 54100 Current children cumulated CPU time (s) 1039.16 Current children cumulated vsize (Kb) 56224 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 104827 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0 [pid=23051] vsize: 54100 Current children cumulated CPU time (s) 1049.17 Current children cumulated vsize (Kb) 56224 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 105826 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0 [pid=23051] vsize: 54100 Current children cumulated CPU time (s) 1059.16 Current children cumulated vsize (Kb) 56224 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 13302 0 0 0 106827 90 0 0 25 0 1 0 1851937192 55398400 12694 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 13525 12694 145 145 0 13380 0 [pid=23051] vsize: 54100 Current children cumulated CPU time (s) 1069.17 Current children cumulated vsize (Kb) 56224 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 14593 0 0 0 107823 93 0 0 25 0 1 0 1851937192 59613184 13695 4294967295 134512640 135094434 3221224432 3221128704 134522857 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 14554 13695 145 145 0 14409 0 [pid=23051] vsize: 58216 Current children cumulated CPU time (s) 1079.16 Current children cumulated vsize (Kb) 60340 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18084 0 0 0 108796 107 0 0 25 0 1 0 1851937192 76156928 17174 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18593 17174 145 145 0 18448 0 [pid=23051] vsize: 74372 Current children cumulated CPU time (s) 1089.03 Current children cumulated vsize (Kb) 76496 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18084 0 0 0 109797 107 0 0 25 0 1 0 1851937192 76156928 17174 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18593 17174 145 145 0 18448 0 [pid=23051] vsize: 74372 Current children cumulated CPU time (s) 1099.04 Current children cumulated vsize (Kb) 76496 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18088 0 0 0 110797 107 0 0 25 0 1 0 1851937192 76173312 17178 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18597 17178 145 145 0 18452 0 [pid=23051] vsize: 74388 Current children cumulated CPU time (s) 1109.04 Current children cumulated vsize (Kb) 76512 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18102 0 0 0 111797 107 0 0 25 0 1 0 1851937192 76238848 17192 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18613 17192 145 145 0 18468 0 [pid=23051] vsize: 74452 Current children cumulated CPU time (s) 1119.04 Current children cumulated vsize (Kb) 76576 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18107 0 0 0 112797 107 0 0 25 0 1 0 1851937192 76255232 17197 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17197 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1129.04 Current children cumulated vsize (Kb) 76592 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18114 0 0 0 113797 107 0 0 25 0 1 0 1851937192 76255232 17204 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17204 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1139.04 Current children cumulated vsize (Kb) 76592 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 114798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1149.05 Current children cumulated vsize (Kb) 76592 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 115798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1159.05 Current children cumulated vsize (Kb) 76592 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 116798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1169.05 Current children cumulated vsize (Kb) 76592 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 117798 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1179.05 Current children cumulated vsize (Kb) 76592 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 118799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1189.06 Current children cumulated vsize (Kb) 76592 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 119799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1199.06 Current children cumulated vsize (Kb) 76592 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 120799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1209.06 Current children cumulated vsize (Kb) 76592 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 23051 Raw data (/proc/23047/stat): 23047 (minisat+_script) S 23046 23047 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851937187 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/23047/statm): 531 226 485 147 0 384 0 [pid=23047] vsize: 2124 Raw data (/proc/23051/stat): 23051 (minisat+_64-bit) R 23047 23047 2660 0 -1 0 18117 0 0 0 120799 107 0 0 25 0 1 0 1851937192 76255232 17207 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/23051/statm): 18617 17207 145 145 0 18472 0 [pid=23051] vsize: 74468 Current children cumulated CPU time (s) 1209.06 Current children cumulated vsize (Kb) 76592 Sending SIGTERM to -23047 Sleeping 2 seconds One traced child (pid=23047) ended because it received signal 15 (SIGTERM) One traced child (pid=23051) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1209.11 CPU user time (s): 1208 CPU system time (s): 1.11383 CPU usage (%): 99.9142 Max. virtual memory (cumulated for all children) (Kb): 76592
ERROR: no interpretation found !