| Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-misc05.opb |
| MD5SUM | 5e97a4ad772c87cdf15a611dd5b54048 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 1076796928 |
| Optimality of the best value was proved | YES |
| Number of terms in the objective function | 31 |
| Biggest coefficient in the objective function | 1073741824 |
| Number of bits for the biggest coefficient in the objective function | 31 |
| Sum of the numbers in the objective function | 2147483647 |
| Number of bits of the sum of numbers in the objective function | 31 |
| Biggest number in a constraint | 5368709120 |
| Number of bits of the biggest number in a constraint | 33 |
| Biggest sum of numbers in a constraint | 83751857084 |
| Number of bits of the biggest sum of numbers | 37 |
| Best result obtained on this benchmark | OPTIMUM FOUND |
| Best CPU time to get the best result obtained on this benchmark | 968.747 |
| Number of variables | 1940 |
| Total number of constraints | 374 |
| Number of constraints which are clauses | 155 |
| Number of constraints which are cardinality constraints (but not clauses) | 82 |
| Number of constraints which are nor clauses,nor cardinality constraints | 137 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 451 |
LAUNCH ON wulflinc19 THE 2005-09-19 03:09:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2865 boxname=wulflinc19 idbench=521 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5e97a4ad772c87cdf15a611dd5b54048 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-misc05.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-misc05.opb IDLAUNCH: 2865 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 887520 kB Buffers: 35896 kB Cached: 84108 kB SwapCached: 832 kB Active: 72892 kB Inactive: 49712 kB HighTotal: 131008 kB HighFree: 46116 kB LowTotal: 903652 kB LowFree: 841404 kB SwapTotal: 2097892 kB SwapFree: 2096460 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18916 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:25:45 (client local time) WITH STATUS 30 IN 968.747 SECONDS stats: 2865 0 968.747 30
c Parsing PB file... c Converting 327 PB-constraints to clauses... c -- Unit propagations: ppppppppppp c -- Detecting intervals from adjacent constraints: ############################ c -- Clauses(.)/Splits(s): ...............................................................................................................................ssssssssssssssssssssssss c ---[ 349]---> Adder-cost: 124 maxlim: 3219483647 bits: 33/32 c ---[ 345]---> Adder-cost: 876 maxlim: 5368714235 bits: 34/33 c ---[ 343]---> Sorter-cost: 5504 Base: 2 2 2 2 2 2 2 2 2 3 5 2 2 2 17 2 2 2 2 2 2 2 2 2 c ---[ 341]---> BDD-cost: 13 c ---[ 339]---> BDD-cost: 13 c ---[ 337]---> BDD-cost: 13 c ---[ 335]---> BDD-cost: 11 c ---[ 333]---> BDD-cost: 13 c ---[ 331]---> BDD-cost: 13 c ---[ 329]---> BDD-cost: 13 c ---[ 200]---> Sorter-cost: 118 Base: c ---[ 198]---> Sorter-cost: 127 Base: c ---[ 196]---> Sorter-cost: 126 Base: c ---[ 194]---> Sorter-cost: 119 Base: c ---[ 192]---> Sorter-cost: 126 Base: c ---[ 190]---> Sorter-cost: 123 Base: c ---[ 188]---> Sorter-cost: 126 Base: c ---[ 186]---> Sorter-cost: 127 Base: c ---[ 184]---> Sorter-cost: 127 Base: c ---[ 182]---> Adder-cost: 443 maxlim: 1880058 bits: 22/21 c ---[ 180]---> Adder-cost: 492 maxlim: 3186682 bits: 23/22 c ---[ 178]---> Adder-cost: 492 maxlim: 3350522 bits: 23/22 c ---[ 176]---> Adder-cost: 443 maxlim: 1566715 bits: 22/21 c ---[ 174]---> Adder-cost: 492 maxlim: 3207162 bits: 23/22 c ---[ 172]---> Adder-cost: 492 maxlim: 3176442 bits: 23/22 c ---[ 170]---> Adder-cost: 492 maxlim: 3330042 bits: 23/22 c ---[ 168]---> BDD-cost: 89 c ---[ 166]---> BDD-cost: 89 c ---[ 165]---> Sorter-cost: 1941 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 1941 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> BDD-cost: 148 c ---[ 134]---> BDD-cost: 23 c ---[ 133]---> BDD-cost: 23 c ---[ 132]---> BDD-cost: 23 c ---[ 131]---> BDD-cost: 23 c ---[ 130]---> BDD-cost: 23 c ---[ 129]---> BDD-cost: 23 c ---[ 128]---> BDD-cost: 26 c ---[ 127]---> BDD-cost: 26 c ---[ 126]---> BDD-cost: 26 c ---[ 125]---> BDD-cost: 26 c ---[ 124]---> BDD-cost: 26 c ---[ 123]---> BDD-cost: 26 c ---[ 122]---> BDD-cost: 26 c ---[ 121]---> BDD-cost: 26 c ---[ 120]---> BDD-cost: 26 c ---[ 119]---> BDD-cost: 26 c ---[ 118]---> BDD-cost: 26 c ---[ 117]---> BDD-cost: 26 c ---[ 115]---> BDD-cost: 25 c ---[ 114]---> BDD-cost: 25 c ---[ 113]---> BDD-cost: 25 c ---[ 112]---> BDD-cost: 25 c ---[ 111]---> BDD-cost: 25 c ---[ 110]---> BDD-cost: 25 c ---[ 109]---> BDD-cost: 25 c ---[ 108]---> BDD-cost: 25 c ---[ 107]---> BDD-cost: 25 c ---[ 106]---> BDD-cost: 25 c ---[ 105]---> BDD-cost: 25 c ---[ 104]---> BDD-cost: 27 c ---[ 103]---> BDD-cost: 27 c ---[ 102]---> BDD-cost: 27 c ---[ 101]---> BDD-cost: 27 c ---[ 100]---> BDD-cost: 27 c ---[ 99]---> BDD-cost: 27 c ---[ 98]---> BDD-cost: 22 c ---[ 97]---> BDD-cost: 22 c ---[ 96]---> BDD-cost: 22 c ---[ 95]---> BDD-cost: 22 c ---[ 94]---> BDD-cost: 22 c ---[ 93]---> BDD-cost: 22 c ---[ 92]---> BDD-cost: 26 c ---[ 91]---> BDD-cost: 26 c ---[ 90]---> BDD-cost: 26 c ---[ 89]---> BDD-cost: 26 c ---[ 88]---> BDD-cost: 26 c ---[ 87]---> BDD-cost: 26 c ---[ 86]---> BDD-cost: 26 c ---[ 85]---> BDD-cost: 26 c ---[ 84]---> BDD-cost: 26 c ---[ 83]---> BDD-cost: 26 c ---[ 82]---> BDD-cost: 26 c ---[ 81]---> BDD-cost: 26 c ---[ 80]---> BDD-cost: 26 c ---[ 79]---> BDD-cost: 26 c ---[ 77]---> BDD-cost: 5 c ---[ 76]---> BDD-cost: 7 c ---[ 73]---> BDD-cost: 6 c ---[ 72]---> BDD-cost: 7 c ---[ 71]---> BDD-cost: 6 c ---[ 70]---> BDD-cost: 8 c ---[ 67]---> BDD-cost: 7 c ---[ 66]---> BDD-cost: 7 c ---[ 64]---> BDD-cost: 8 c ---[ 61]---> BDD-cost: 7 c ---[ 59]---> BDD-cost: 5 c ---[ 56]---> BDD-cost: 6 c ---[ 55]---> BDD-cost: 7 c ---[ 53]---> BDD-cost: 6 c ---[ 52]---> BDD-cost: 8 c ---[ 50]---> BDD-cost: 7 c ---[ 49]---> BDD-cost: 7 c ---[ 47]---> BDD-cost: 6 c ---[ 46]---> BDD-cost: 8 c ---[ 44]---> BDD-cost: 7 c ---[ 43]---> BDD-cost: 7 c ---[ 41]---> BDD-cost: 6 c ---[ 40]---> BDD-cost: 8 c ---[ 37]---> BDD-cost: 7 c ---[ 35]---> BDD-cost: 6 c ---[ 34]---> BDD-cost: 8 c ---[ 31]---> BDD-cost: 7 c ---[ 30]---> BDD-cost: 7 c ---[ 28]---> BDD-cost: 6 c ---[ 27]---> BDD-cost: 8 c ---[ 24]---> BDD-cost: 7 c ---[ 23]---> BDD-cost: 3 c ---[ 22]---> BDD-cost: 4 c ---[ 21]---> BDD-cost: 4 c ---[ 20]---> BDD-cost: 4 c ---[ 19]---> BDD-cost: 4 c ---[ 18]---> BDD-cost: 3 c ---[ 17]---> BDD-cost: 4 c ---[ 16]---> BDD-cost: 4 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 4 c ---[ 13]---> BDD-cost: 4 c ---[ 12]---> BDD-cost: 3 c ---[ 11]---> BDD-cost: 4 c ---[ 10]---> BDD-cost: 3 c ---[ 9]---> BDD-cost: 4 c ---[ 8]---> BDD-cost: 3 c ---[ 7]---> BDD-cost: 4 c ---[ 6]---> BDD-cost: 4 c ---[ 5]---> BDD-cost: 3 c ---[ 4]---> BDD-cost: 4 c ---[ 3]---> BDD-cost: 4 c ---[ 2]---> BDD-cost: 3 c ---[ 1]---> BDD-cost: 4 c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 58171 173898 | 19390 0 0 nan | 0.000 % | c | 101 | 58132 173812 | 21329 97 7432 76.6 | 8.780 % | c | 251 | 57582 172244 | 23461 238 11120 46.7 | 9.366 % | c | 476 | 57522 172103 | 25808 449 15016 33.4 | 9.465 % | c | 814 | 57285 171316 | 28388 597 15054 25.2 | 9.644 % | c | 1320 | 56930 170167 | 31227 1085 26049 24.0 | 9.952 % | c | 2079 | 56586 169348 | 34350 1816 45304 24.9 | 10.526 % | c | 3218 | 56489 169107 | 37785 2938 82358 28.0 | 10.699 % | c | 4926 | 56311 168498 | 41564 4556 218527 48.0 | 10.835 % | c ============================================================================== c [1mFound solution: 1076964352[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5271 | 55995 167536 | 18665 4830 225170 46.6 | 10.835 % | c ============================================================================== c [1mFound solution: 1076947456[0m c ---[ 0]---> BDD-cost: 21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5340 | 55507 166422 | 18502 4890 226414 46.3 | 10.835 % | c | 5442 | 55507 166422 | 20352 4992 236085 47.3 | 12.149 % | c ============================================================================== c [1mFound solution: 1076900864[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5569 | 55528 166469 | 18509 5119 244096 47.7 | 12.149 % | c | 5670 | 55528 166469 | 20359 5220 247204 47.4 | 12.150 % | c | 5821 | 55519 166438 | 22395 5369 250573 46.7 | 12.157 % | c | 6047 | 52914 160284 | 24635 5564 255118 45.9 | 16.741 % | c | 6384 | 52862 160158 | 27099 5893 271670 46.1 | 16.821 % | c | 6890 | 52862 160158 | 29808 6399 333114 52.1 | 16.821 % | c | 7650 | 52352 158884 | 32789 7124 352380 49.5 | 17.671 % | c | 8789 | 52222 158565 | 36068 8253 414040 50.2 | 17.905 % | c | 10497 | 52134 158263 | 39675 9932 485154 48.8 | 17.961 % | c | 13061 | 52051 157993 | 43643 12452 585909 47.1 | 18.047 % | c | 16905 | 51977 157757 | 48007 16281 758756 46.6 | 18.108 % | c ============================================================================== c [1mFound solution: 1076880384[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21950 | 51156 155790 | 17052 21253 1085951 51.1 | 18.108 % | c | 22050 | 51156 155790 | 18757 10727 513729 47.9 | 19.654 % | c | 22200 | 51156 155790 | 20632 10877 520756 47.9 | 19.654 % | c | 22427 | 51156 155790 | 22696 11104 540071 48.6 | 19.654 % | c | 22764 | 51156 155790 | 24965 11441 575411 50.3 | 19.654 % | c | 23271 | 51111 155635 | 27462 11938 591452 49.5 | 19.685 % | c | 24030 | 51093 155573 | 30208 12694 630406 49.7 | 19.697 % | c | 25170 | 51050 155442 | 33229 13822 699257 50.6 | 19.752 % | c | 26879 | 51001 155278 | 36552 15522 821447 52.9 | 19.789 % | c ============================================================================== c [1mFound solution: 1076868608[0m c ---[ 0]---> BDD-cost: 21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28936 | 50882 154867 | 16960 17540 949700 54.1 | 19.789 % | c | 29039 | 50882 154867 | 18656 17643 952141 54.0 | 19.895 % | c | 29190 | 50882 154867 | 20521 17794 969905 54.5 | 19.895 % | c | 29421 | 50882 154867 | 22573 18025 979052 54.3 | 19.895 % | c | 29758 | 50882 154867 | 24831 18362 1014438 55.2 | 19.895 % | c | 30265 | 50091 152926 | 27314 18809 1073650 57.1 | 21.360 % | c ============================================================================== c [1mFound solution: 1076843520[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30530 | 49814 152283 | 16604 19065 1098747 57.6 | 21.360 % | c | 30631 | 49814 152283 | 18264 19166 1100477 57.4 | 21.952 % | c | 30781 | 49806 152257 | 20090 19315 1109769 57.5 | 21.958 % | c | 31006 | 49806 152257 | 22099 19540 1119143 57.3 | 21.958 % | c | 31343 | 49806 152257 | 24309 19877 1133582 57.0 | 21.958 % | c | 31849 | 49748 152122 | 26740 20378 1168990 57.4 | 22.075 % | c | 32609 | 49748 152122 | 29414 21138 1222866 57.9 | 22.075 % | c | 33749 | 49748 152122 | 32356 22278 1286227 57.7 | 22.075 % | c | 35457 | 49739 152091 | 35592 23984 1483501 61.9 | 22.081 % | c | 38019 | 49681 151919 | 39151 26538 1757628 66.2 | 22.148 % | c | 41864 | 49646 151808 | 43066 30377 2481999 81.7 | 22.179 % | c ============================================================================== c [1mFound solution: 1076835840[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43893 | 49635 151755 | 16545 32404 2805306 86.6 | 22.179 % | c | 43993 | 49635 151755 | 18199 16302 1661740 101.9 | 22.202 % | c | 44144 | 49635 151755 | 20019 16453 1668912 101.4 | 22.202 % | c | 44370 | 49635 151755 | 22021 16679 1733512 103.9 | 22.202 % | c | 44708 | 49635 151755 | 24223 17017 1789160 105.1 | 22.202 % | c | 45215 | 49571 151535 | 26645 17510 1828409 104.4 | 22.263 % | c | 45976 | 49571 151535 | 29310 18271 2002629 109.6 | 22.263 % | c | 47115 | 49557 151487 | 32241 19409 2134532 110.0 | 22.269 % | c ============================================================================== c [1mFound solution: 1076831744[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47596 | 49577 151534 | 16525 19890 2181717 109.7 | 22.269 % | c | 47697 | 49577 151534 | 18177 19991 2191723 109.6 | 22.265 % | c | 47847 | 49577 151534 | 19995 20141 2207453 109.6 | 22.265 % | c | 48072 | 49577 151534 | 21994 20366 2236047 109.8 | 22.265 % | c | 48410 | 49577 151534 | 24194 20704 2278546 110.1 | 22.265 % | c | 48921 | 49559 151472 | 26613 21213 2366062 111.5 | 22.277 % | c | 49683 | 49550 151441 | 29275 21974 2515580 114.5 | 22.283 % | c | 50825 | 49550 151441 | 32202 23116 2608821 112.9 | 22.283 % | c | 52533 | 49541 151410 | 35422 24822 2925765 117.9 | 22.289 % | c ============================================================================== c [1mFound solution: 1076822016[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 55046 | 49548 151428 | 16516 27334 3394217 124.2 | 22.289 % | c | 55148 | 49548 151428 | 18167 13769 1320369 95.9 | 22.301 % | c | 55299 | 49548 151428 | 19984 13920 1345783 96.7 | 22.301 % | c | 55525 | 49548 151428 | 21982 14146 1384925 97.9 | 22.301 % | c | 55866 | 49548 151428 | 24181 14487 1429569 98.7 | 22.301 % | c | 56372 | 49548 151428 | 26599 14993 1516898 101.2 | 22.301 % | c | 57131 | 49548 151428 | 29259 15752 1623288 103.1 | 22.301 % | c | 58271 | 49548 151428 | 32185 16892 1856440 109.9 | 22.301 % | c | 59979 | 49548 151428 | 35403 18600 2153057 115.8 | 22.301 % | c | 62544 | 49548 151428 | 38943 21165 2645957 125.0 | 22.301 % | c | 66390 | 49483 151284 | 42838 25004 2947670 117.9 | 22.405 % | c ============================================================================== c [1mFound solution: 1076801024[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69269 | 49506 151338 | 16502 27883 3500976 125.6 | 22.405 % | c | 69372 | 49506 151338 | 18152 14045 1208054 86.0 | 22.396 % | c | 69522 | 49506 151338 | 19967 14195 1235914 87.1 | 22.396 % | c | 69748 | 49506 151338 | 21964 14421 1270763 88.1 | 22.396 % | c ============================================================================== c [1mFound solution: 1076796928[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69837 | 49518 151356 | 16506 14507 1283000 88.4 | 22.396 % | c | 69938 | 49518 151356 | 18156 14608 1298896 88.9 | 22.396 % | c | 70090 | 49518 151356 | 19972 14760 1325230 89.8 | 22.396 % | c | 70317 | 49518 151356 | 21969 14987 1360231 90.8 | 22.396 % | c | 70654 | 49518 151356 | 24166 15324 1394300 91.0 | 22.396 % | c | 71160 | 49518 151356 | 26583 15830 1522421 96.2 | 22.396 % | c | 71919 | 49510 151338 | 29241 16588 1677890 101.2 | 22.408 % | c | 73059 | 49510 151338 | 32165 17728 1868791 105.4 | 22.408 % | c | 74767 | 49510 151338 | 35382 19436 2217347 114.1 | 22.408 % | c | 77329 | 49510 151338 | 38920 21998 2800862 127.3 | 22.408 % | c | 81174 | 49496 151290 | 42812 25842 3410796 132.0 | 22.415 % | c | 86940 | 49413 151046 | 47093 31599 4280012 135.4 | 22.519 % | c | 95596 | 49387 150958 | 51802 40250 5527965 137.3 | 22.537 % | c | 108572 | 49387 150958 | 56983 53226 8269961 155.4 | 22.537 % | c | 128033 | 49293 150700 | 62681 35170 5094862 144.9 | 22.672 % | c | 157225 | 49276 150651 | 68949 64359 9964945 154.8 | 22.691 % | c ============================================================================== c [1mOptimal solution: 1076796928[0m s OPTIMUM FOUND v -COL133_bit_10 -COL133_bit_9 -COL133_bit_8 -COL133_bit_7 -COL133_bit_6 -COL133_bit_5 -COL133_bit_4 -COL133_bit_3 -COL133_bit_2 COL133_bit_1 COL133_bit0 COL133_bit1 COL133_bit2 -COL133_bit3 -COL133_bit4 COL133_bit5 -COL133_bit6 COL133_bit7 COL133_bit8 COL133_bit9 -COL133_bit10 COL133_bit11 -COL133_bit12 -COL133_bit13 -COL133_bit14 -COL133_bit15 -COL133_bit16 -COL133_bit17 -COL133_bit18 -COL133_bit19 COL133_bit20 -COL001_bit0 -COL002_bit0 -COL003_bit0 -COL004_bit0 -COL005_bit0 -COL006_bit0 COL007_bit0 -COL008_bit0 COL009_bit0 -COL010_bit0 -COL011_bit0 -COL012_bit0 -COL013_bit0 -COL014_bit0 -COL015_bit0 -COL016_bit0 -COL017_bit0 -COL018_bit0 -COL019_bit0 -COL020_bit0 -COL021_bit0 -COL022_bit0 COL023_bit0 -COL024_bit0 -COL025_bit0 -COL026_bit0 COL027_bit0 -COL028_bit0 -COL029_bit0 -COL030_bit0 -COL031_bit0 -COL032_bit0 -COL033_bit0 -COL034_bit0 -COL035_bit0 -COL036_bit0 COL037_bit0 -COL038_bit0 -COL039_bit0 -COL040_bit0 -COL041_bit0 -COL042_bit0 -COL043_bit0 -COL044_bit0 -COL045_bit0 -COL046_bit0 -COL047_bit0 COL048_bit0 -COL049_bit0 -COL050_bit0 -COL051_bit0 -COL052_bit0 -COL053_bit0 -COL054_bit0 -COL055_bit0 COL056_bit0 -COL057_bit0 COL058_bit0 -COL059_bit0 COL060_bit0 -COL061_bit0 -COL062_bit0 -COL063_bit0 -COL064_bit0 -COL065_bit0 -COL066_bit0 -COL067_bit0 -COL068_bit0 COL069_bit0 -COL070_bit0 COL071_bit0 -COL072_bit0 COL129_bit0 COL130_bit0 -COL134_bit_10 -COL134_bit_9 -COL134_bit_8 -COL134_bit_7 -COL134_bit_6 -COL134_bit_5 -COL134_bit_4 -COL134_bit_3 -COL134_bit_2 -COL134_bit_1 COL134_bit0 COL134_bit1 -COL134_bit2 -COL134_bit3 -COL134_bit4 COL134_bit5 -COL134_bit6 COL134_bit7 -COL134_bit8 COL134_bit9 COL134_bit10 -COL134_bit11 -COL134_bit12 -COL134_bit13 -COL134_bit14 -COL134_bit15 -COL134_bit16 -COL134_bit17 -COL134_bit18 -COL134_bit19 COL134_bit20 -COL135_bit_10 -COL135_bit_9 -COL135_bit_8 -COL135_bit_7 -COL135_bit_6 -COL135_bit_5 -COL135_bit_4 -COL135_bit_3 -COL135_bit_2 -COL135_bit_1 COL135_bit0 -COL135_bit1 COL135_bit2 -COL135_bit3 -COL135_bit4 -COL135_bit5 -COL135_bit6 COL135_bit7 COL135_bit8 COL135_bit9 -COL135_bit10 -COL135_bit11 -COL135_bit12 -COL135_bit13 -COL135_bit14 -COL135_bit15 -COL135_bit16 -COL135_bit17 -COL135_bit18 -COL135_bit19 COL135_bit20 -COL136_bit_10 -COL136_bit_9 -COL136_bit_8 -COL136_bit_7 -COL136_bit_6 -COL136_bit_5 -COL136_bit_4 -COL136_bit_3 -COL136_bit_2 COL136_bit_1 COL136_bit0 -COL136_bit1 COL136_bit2 COL136_bit3 COL136_bit4 COL136_bit5 COL136_bit6 -COL136_bit7 COL136_bit8 -COL136_bit9 -COL136_bit10 -COL136_bit11 -COL136_bit12 -COL136_bit13 -COL136_bit14 -COL136_bit15 -COL136_bit16 -COL136_bit17 -COL136_bit18 -COL136_bit19 COL136_bit20 -COL115_bit_10 -COL115_bit_9 -COL115_bit_8 -COL115_bit_7 -COL115_bit_6 -COL115_bit_5 -COL115_bit_4 -COL115_bit_3 -COL115_bit_2 -COL115_bit_1 -COL115_bit0 -COL115_bit1 -COL115_bit2 -COL115_bit3 -COL115_bit4 -COL115_bit5 -COL115_bit6 -COL115_bit7 -COL115_bit8 -COL115_bit9 -COL115_bit10 -COL115_bit11 -COL115_bit12 -COL115_bit13 -COL115_bit14 -COL115_bit15 -COL115_bit16 -COL115_bit17 -COL115_bit18 -COL115_bit19 -COL116_bit_10 -COL116_bit_9 -COL116_bit_8 -COL116_bit_7 -COL116_bit_6 -COL116_bit_5 -COL116_bit_4 -COL116_bit_3 -COL116_bit_2 -COL116_bit_1 -COL116_bit0 -COL116_bit1 COL116_bit2 -COL116_bit3 COL116_bit4 -COL116_bit5 COL116_bit6 -COL116_bit7 COL116_bit8 -COL116_bit9 -COL116_bit10 -COL116_bit11 -COL116_bit12 -COL116_bit13 -COL116_bit14 -COL116_bit15 -COL116_bit16 -COL116_bit17 -COL116_bit18 -COL116_bit19 -COL117_bit_10 -COL117_bit_9 -COL117_bit_8 -COL117_bit_7 -COL117_bit_6 -COL117_bit_5 -COL117_bit_4 -COL117_bit_3 -COL117_bit_2 -COL117_bit_1 -COL117_bit0 -COL117_bit1 -COL117_bit2 -COL117_bit3 -COL117_bit4 -COL117_bit5 -COL117_bit6 -COL117_bit7 -COL117_bit8 -COL117_bit9 -COL117_bit10 -COL117_bit11 -COL117_bit12 -COL117_bit13 -COL117_bit14 -COL117_bit15 -COL117_bit16 -COL117_bit17 -COL117_bit18 -COL117_bit19 -COL118_bit_10 -COL118_bit_9 -COL118_bit_8 -COL118_bit_7 -COL118_bit_6 -COL118_bit_5 -COL118_bit_4 -COL118_bit_3 -COL118_bit_2 -COL118_bit_1 -COL118_bit0 COL118_bit1 -COL118_bit2 -COL118_bit3 -COL118_bit4 -COL118_bit5 COL118_bit6 COL118_bit7 COL118_bit8 -COL118_bit9 -COL118_bit10 -COL118_bit11 -COL118_bit12 -COL118_bit13 -COL118_bit14 -COL118_bit15 -COL118_bit16 -COL118_bit17 -COL118_bit18 -COL118_bit19 -COL119_bit_10 -COL119_bit_9 -COL119_bit_8 -COL119_bit_7 -COL119_bit_6 -COL119_bit_5 -COL119_bit_4 -COL119_bit_3 -COL119_bit_2 -COL119_bit_1 -COL119_bit0 -COL119_bit1 -COL119_bit2 -COL119_bit3 -COL119_bit4 -COL119_bit5 -COL119_bit6 -COL119_bit7 -COL119_bit8 -COL119_bit9 -COL119_bit10 -COL119_bit11 -COL119_bit12 -COL119_bit13 -COL119_bit14 -COL119_bit15 -COL119_bit16 -COL119_bit17 -COL119_bit18 -COL119_bit19 -COL120_bit_10 -COL120_bit_9 -COL120_bit_8 -COL120_bit_7 -COL120_bit_6 -COL120_bit_5 -COL120_bit_4 -COL120_bit_3 -COL120_bit_2 -COL120_bit_1 -COL120_bit0 -COL120_bit1 -COL120_bit2 -COL120_bit3 -COL120_bit4 -COL120_bit5 -COL120_bit6 -COL120_bit7 -COL120_bit8 -COL120_bit9 -COL120_bit10 -COL120_bit11 -COL120_bit12 -COL120_bit13 -COL120_bit14 -COL120_bit15 -COL120_bit16 -COL120_bit17 -COL120_bit18 -COL120_bit19 -COL121_bit_10 -COL121_bit_9 -COL121_bit_8 -COL121_bit_7 -COL121_bit_6 -COL121_bit_5 -COL121_bit_4 -COL121_bit_3 -COL121_bit_2 -COL121_bit_1 -COL121_bit0 -COL121_bit1 -COL121_bit2 -COL121_bit3 -COL121_bit4 -COL121_bit5 -COL121_bit6 -COL121_bit7 -COL121_bit8 -COL121_bit9 -COL121_bit10 -COL121_bit11 -COL121_bit12 -COL121_bit13 -COL121_bit14 -COL121_bit15 -COL121_bit16 -COL121_bit17 -COL121_bit18 -COL121_bit19 -COL122_bit_10 -COL122_bit_9 -COL122_bit_8 -COL122_bit_7 -COL122_bit_6 -COL122_bit_5 -COL122_bit_4 -COL122_bit_3 -COL122_bit_2 -COL122_bit_1 -COL122_bit0 -COL122_bit1 -COL122_bit2 -COL122_bit3 -COL122_bit4 -COL122_bit5 -COL122_bit6 -COL122_bit7 -COL122_bit8 -COL122_bit9 -COL122_bit10 -COL122_bit11 -COL122_bit12 -COL122_bit13 -COL122_bit14 -COL122_bit15 -COL122_bit16 -COL122_bit17 -COL122_bit18 -COL122_bit19 -COL123_bit_10 -COL123_bit_9 -COL123_bit_8 -COL123_bit_7 -COL123_bit_6 -COL123_bit_5 -COL123_bit_4 -COL123_bit_3 -COL123_bit_2 -COL123_bit_1 -COL123_bit0 -COL123_bit1 -COL123_bit2 -COL123_bit3 -COL123_bit4 -COL123_bit5 -COL123_bit6 -COL123_bit7 -COL123_bit8 -COL123_bit9 -COL123_bit10 -COL123_bit11 -COL123_bit12 -COL123_bit13 -COL123_bit14 -COL123_bit15 -COL123_bit16 -COL123_bit17 -COL123_bit18 -COL123_bit19 -COL124_bit_10 -COL124_bit_9 -COL124_bit_8 -COL124_bit_7 -COL124_bit_6 -COL124_bit_5 -COL124_bit_4 -COL124_bit_3 -COL124_bit_2 -COL124_bit_1 -COL124_bit0 -COL124_bit1 -COL124_bit2 -COL124_bit3 -COL124_bit4 -COL124_bit5 -COL124_bit6 -COL124_bit7 -COL124_bit8 -COL124_bit9 -COL124_bit10 -COL124_bit11 -COL124_bit12 -COL124_bit13 -COL124_bit14 -COL124_bit15 -COL124_bit16 -COL124_bit17 -COL124_bit18 -COL124_bit19 -COL125_bit_10 -COL125_bit_9 -COL125_bit_8 -COL125_bit_7 -COL125_bit_6 -COL125_bit_5 -COL125_bit_4 -COL125_bit_3 -COL125_bit_2 -COL125_bit_1 -COL125_bit0 -COL125_bit1 -COL125_bit2 -COL125_bit3 -COL125_bit4 -COL125_bit5 -COL125_bit6 -COL125_bit7 -COL125_bit8 -COL125_bit9 -COL125_bit10 -COL125_bit11 -COL125_bit12 -COL125_bit13 -COL125_bit14 -COL125_bit15 -COL125_bit16 -COL125_bit17 -COL125_bit18 -COL125_bit19 -COL126_bit_10 -COL126_bit_9 -COL126_bit_8 -COL126_bit_7 -COL126_bit_6 -COL126_bit_5 -COL126_bit_4 -COL126_bit_3 -COL126_bit_2 -COL126_bit_1 -COL126_bit0 COL126_bit1 -COL126_bit2 COL126_bit3 COL126_bit4 -COL126_bit5 COL126_bit6 -COL126_bit7 -COL126_bit8 -COL126_bit9 -COL126_bit10 -COL126_bit11 -COL126_bit12 -COL126_bit13 -COL126_bit14 -COL126_bit15 -COL126_bit16 -COL126_bit17 -COL126_bit18 -COL126_bit19 -COL127_bit_10 -COL127_bit_9 -COL127_bit_8 -COL127_bit_7 -COL127_bit_6 -COL127_bit_5 -COL127_bit_4 -COL127_bit_3 -COL127_bit_2 -COL127_bit_1 -COL127_bit0 -COL127_bit1 -COL127_bit2 -COL127_bit3 -COL127_bit4 -COL127_bit5 -COL127_bit6 -COL127_bit7 -COL127_bit8 -COL127_bit9 -COL127_bit10 -COL127_bit11 -COL127_bit12 -COL127_bit13 -COL127_bit14 -COL127_bit15 -COL127_bit16 -COL127_bit17 -COL127_bit18 -COL127_bit19 -COL128_bit_10 -COL128_bit_9 -COL128_bit_8 -COL128_bit_7 -COL128_bit_6 -COL128_bit_5 -COL128_bit_4 -COL128_bit_3 -COL128_bit_2 -COL128_bit_1 -COL128_bit0 -COL128_bit1 COL128_bit2 -COL128_bit3 COL128_bit4 COL128_bit5 -COL128_bit6 COL128_bit7 -COL128_bit8 -COL128_bit9 -COL128_bit10 -COL128_bit11 -COL128_bit12 -COL128_bit13 -COL128_bit14 -COL128_bit15 -COL128_bit16 -COL128_bit17 -COL128_bit18 -COL128_bit19 -COL073_bit_10 -COL073_bit_9 -COL073_bit_8 -COL073_bit_7 -COL073_bit_6 -COL073_bit_5 -COL073_bit_4 -COL073_bit_3 -COL073_bit_2 -COL073_bit_1 -COL073_bit0 -COL073_bit1 -COL073_bit2 -COL073_bit3 -COL073_bit4 -COL073_bit5 -COL073_bit6 -COL073_bit7 -COL073_bit8 -COL073_bit9 -COL073_bit10 -COL073_bit11 -COL073_bit12 -COL073_bit13 -COL073_bit14 -COL073_bit15 -COL073_bit16 -COL073_bit17 -COL073_bit18 -COL073_bit19 -COL074_bit_10 -COL074_bit_9 -COL074_bit_8 -COL074_bit_7 -COL074_bit_6 -COL074_bit_5 -COL074_bit_4 -COL074_bit_3 -COL074_bit_2 -COL074_bit_1 -COL074_bit0 -COL074_bit1 -COL074_bit2 -COL074_bit3 -COL074_bit4 -COL074_bit5 -COL074_bit6 -COL074_bit7 -COL074_bit8 -COL074_bit9 -COL074_bit10 -COL074_bit11 -COL074_bit12 -COL074_bit13 -COL074_bit14 -COL074_bit15 -COL074_bit16 -COL074_bit17 -COL074_bit18 -COL074_bit19 -COL075_bit_10 -COL075_bit_9 -COL075_bit_8 -COL075_bit_7 -COL075_bit_6 -COL075_bit_5 -COL075_bit_4 -COL075_bit_3 -COL075_bit_2 -COL075_bit_1 -COL075_bit0 -COL075_bit1 -COL075_bit2 -COL075_bit3 -COL075_bit4 -COL075_bit5 -COL075_bit6 -COL075_bit7 -COL075_bit8 -COL075_bit9 -COL075_bit10 -COL075_bit11 -COL075_bit12 -COL075_bit13 -COL075_bit14 -COL075_bit15 -COL075_bit16 -COL075_bit17 -COL075_bit18 -COL075_bit19 -COL076_bit_10 -COL076_bit_9 -COL076_bit_8 -COL076_bit_7 -COL076_bit_6 -COL076_bit_5 -COL076_bit_4 -COL076_bit_3 -COL076_bit_2 -COL076_bit_1 -COL076_bit0 -COL076_bit1 -COL076_bit2 -COL076_bit3 -COL076_bit4 -COL076_bit5 -COL076_bit6 -COL076_bit7 -COL076_bit8 -COL076_bit9 -COL076_bit10 -COL076_bit11 -COL076_bit12 -COL076_bit13 -COL076_bit14 -COL076_bit15 -COL076_bit16 -COL076_bit17 -COL076_bit18 -COL076_bit19 -COL077_bit_10 -COL077_bit_9 -COL077_bit_8 -COL077_bit_7 -COL077_bit_6 -COL077_bit_5 -COL077_bit_4 -COL077_bit_3 -COL077_bit_2 -COL077_bit_1 -COL077_bit0 -COL077_bit1 -COL077_bit2 -COL077_bit3 -COL077_bit4 -COL077_bit5 -COL077_bit6 -COL077_bit7 -COL077_bit8 -COL077_bit9 -COL077_bit10 -COL077_bit11 -COL077_bit12 -COL077_bit13 -COL077_bit14 -COL077_bit15 -COL077_bit16 -COL077_bit17 -COL077_bit18 -COL077_bit19 -COL078_bit_10 -COL078_bit_9 -COL078_bit_8 -COL078_bit_7 -COL078_bit_6 -COL078_bit_5 -COL078_bit_4 -COL078_bit_3 -COL078_bit_2 -COL078_bit_1 -COL078_bit0 -COL078_bit1 -COL078_bit2 -COL078_bit3 -COL078_bit4 -COL078_bit5 -COL078_bit6 -COL078_bit7 -COL078_bit8 -COL078_bit9 -COL078_bit10 -COL078_bit11 -COL078_bit12 -COL078_bit13 -COL078_bit14 -COL078_bit15 -COL078_bit16 -COL078_bit17 -COL078_bit18 -COL078_bit19 -COL079_bit_10 -COL079_bit_9 -COL079_bit_8 -COL079_bit_7 -COL079_bit_6 -COL079_bit_5 -COL079_bit_4 -COL079_bit_3 -COL079_bit_2 -COL079_bit_1 -COL079_bit0 -COL079_bit1 COL079_bit2 COL079_bit3 -COL079_bit4 COL079_bit5 -COL079_bit6 -COL079_bit7 COL079_bit8 -COL079_bit9 -COL079_bit10 -COL079_bit11 -COL079_bit12 -COL079_bit13 -COL079_bit14 -COL079_bit15 -COL079_bit16 -COL079_bit17 -COL079_bit18 -COL079_bit19 -COL085_bit_10 -COL085_bit_9 -COL085_bit_8 -COL085_bit_7 -COL085_bit_6 -COL085_bit_5 -COL085_bit_4 -COL085_bit_3 -COL085_bit_2 -COL085_bit_1 -COL085_bit0 -COL085_bit1 -COL085_bit2 -COL085_bit3 -COL085_bit4 -COL085_bit5 -COL085_bit6 -COL085_bit7 -COL085_bit8 -COL085_bit9 -COL085_bit10 -COL085_bit11 -COL085_bit12 -COL085_bit13 -COL085_bit14 -COL085_bit15 -COL085_bit16 -COL085_bit17 -COL085_bit18 -COL085_bit19 -COL091_bit_10 -COL091_bit_9 -COL091_bit_8 -COL091_bit_7 -COL091_bit_6 -COL091_bit_5 -COL091_bit_4 -COL091_bit_3 -COL091_bit_2 -COL091_bit_1 -COL091_bit0 -COL091_bit1 -COL091_bit2 -COL091_bit3 -COL091_bit4 -COL091_bit5 -COL091_bit6 -COL091_bit7 -COL091_bit8 -COL091_bit9 -COL091_bit10 -COL091_bit11 -COL091_bit12 -COL091_bit13 -COL091_bit14 -COL091_bit15 -COL091_bit16 -COL091_bit17 -COL091_bit18 -COL091_bit19 -COL097_bit_10 -COL097_bit_9 -COL097_bit_8 -COL097_bit_7 -COL097_bit_6 -COL097_bit_5 -COL097_bit_4 -COL097_bit_3 -COL097_bit_2 -COL097_bit_1 -COL097_bit0 -COL097_bit1 -COL097_bit2 -COL097_bit3 -COL097_bit4 -COL097_bit5 -COL097_bit6 -COL097_bit7 -COL097_bit8 -COL097_bit9 -COL097_bit10 -COL097_bit11 -COL097_bit12 -COL097_bit13 -COL097_bit14 -COL097_bit15 -COL097_bit16 -COL097_bit17 -COL097_bit18 -COL097_bit19 -COL103_bit_10 -COL103_bit_9 -COL103_bit_8 -COL103_bit_7 -COL103_bit_6 -COL103_bit_5 -COL103_bit_4 -COL103_bit_3 -COL103_bit_2 -COL103_bit_1 -COL103_bit0 -COL103_bit1 -COL103_bit2 -COL103_bit3 -COL103_bit4 -COL103_bit5 -COL103_bit6 -COL103_bit7 -COL103_bit8 -COL103_bit9 -COL103_bit10 -COL103_bit11 -COL103_bit12 -COL103_bit13 -COL103_bit14 -COL103_bit15 -COL103_bit16 -COL103_bit17 -COL103_bit18 -COL103_bit19 -COL109_bit_10 -COL109_bit_9 -COL109_bit_8 -COL109_bit_7 -COL109_bit_6 -COL109_bit_5 -COL109_bit_4 -COL109_bit_3 -COL109_bit_2 -COL109_bit_1 -COL109_bit0 -COL109_bit1 -COL109_bit2 -COL109_bit3 -COL109_bit4 -COL109_bit5 -COL109_bit6 -COL109_bit7 -COL109_bit8 -COL109_bit9 -COL109_bit10 -COL109_bit11 -COL109_bit12 -COL109_bit13 -COL109_bit14 -COL109_bit15 -COL109_bit16 -COL109_bit17 -COL109_bit18 -COL109_bit19 -COL080_bit_10 -COL080_bit_9 -COL080_bit_8 -COL080_bit_7 -COL080_bit_6 -COL080_bit_5 -COL080_bit_4 -COL080_bit_3 -COL080_bit_2 -COL080_bit_1 -COL080_bit0 -COL080_bit1 -COL080_bit2 -COL080_bit3 -COL080_bit4 -COL080_bit5 -COL080_bit6 -COL080_bit7 -COL080_bit8 -COL080_bit9 -COL080_bit10 -COL080_bit11 -COL080_bit12 -COL080_bit13 -COL080_bit14 -COL080_bit15 -COL080_bit16 -COL080_bit17 -COL080_bit18 -COL080_bit19 -COL081_bit_10 -COL081_bit_9 -COL081_bit_8 -COL081_bit_7 -COL081_bit_6 -COL081_bit_5 -COL081_bit_4 -COL081_bit_3 -COL081_bit_2 -COL081_bit_1 -COL081_bit0 -COL081_bit1 -COL081_bit2 -COL081_bit3 -COL081_bit4 -COL081_bit5 -COL081_bit6 -COL081_bit7 -COL081_bit8 -COL081_bit9 -COL081_bit10 -COL081_bit11 -COL081_bit12 -COL081_bit13 -COL081_bit14 -COL081_bit15 -COL081_bit16 -COL081_bit17 -COL081_bit18 -COL081_bit19 -COL082_bit_10 -COL082_bit_9 -COL082_bit_8 -COL082_bit_7 -COL082_bit_6 -COL082_bit_5 -COL082_bit_4 -COL082_bit_3 -COL082_bit_2 -COL082_bit_1 -COL082_bit0 -COL082_bit1 -COL082_bit2 -COL082_bit3 -COL082_bit4 -COL082_bit5 -COL082_bit6 -COL082_bit7 -COL082_bit8 -COL082_bit9 -COL082_bit10 -COL082_bit11 -COL082_bit12 -COL082_bit13 -COL082_bit14 -COL082_bit15 -COL082_bit16 -COL082_bit17 -COL082_bit18 -COL082_bit19 -COL083_bit_10 -COL083_bit_9 -COL083_bit_8 -COL083_bit_7 -COL083_bit_6 -COL083_bit_5 -COL083_bit_4 -COL083_bit_3 -COL083_bit_2 -COL083_bit_1 -COL083_bit0 -COL083_bit1 -COL083_bit2 -COL083_bit3 -COL083_bit4 -COL083_bit5 -COL083_bit6 -COL083_bit7 -COL083_bit8 -COL083_bit9 -COL083_bit10 -COL083_bit11 -COL083_bit12 -COL083_bit13 -COL083_bit14 -COL083_bit15 -COL083_bit16 -COL083_bit17 -COL083_bit18 -COL083_bit19 -COL084_bit_10 -COL084_bit_9 -COL084_bit_8 -COL084_bit_7 -COL084_bit_6 -COL084_bit_5 -COL084_bit_4 -COL084_bit_3 -COL084_bit_2 -COL084_bit_1 -COL084_bit0 -COL084_bit1 -COL084_bit2 -COL084_bit3 -COL084_bit4 -COL084_bit5 -COL084_bit6 -COL084_bit7 -COL084_bit8 -COL084_bit9 -COL084_bit10 -COL084_bit11 -COL084_bit12 -COL084_bit13 -COL084_bit14 -COL084_bit15 -COL084_bit16 -COL084_bit17 -COL084_bit18 -COL084_bit19 -COL086_bit_10 -COL086_bit_9 -COL086_bit_8 -COL086_bit_7 -COL086_bit_6 -COL086_bit_5 -COL086_bit_4 -COL086_bit_3 -COL086_bit_2 -COL086_bit_1 -COL086_bit0 -COL086_bit1 -COL086_bit2 -COL086_bit3 -COL086_bit4 -COL086_bit5 -COL086_bit6 -COL086_bit7 -COL086_bit8 -COL086_bit9 -COL086_bit10 -COL086_bit11 -COL086_bit12 -COL086_bit13 -COL086_bit14 -COL086_bit15 -COL086_bit16 -COL086_bit17 -COL086_bit18 -COL086_bit19 -COL092_bit_10 -COL092_bit_9 -COL092_bit_8 -COL092_bit_7 -COL092_bit_6 -COL092_bit_5 -COL092_bit_4 -COL092_bit_3 -COL092_bit_2 -COL092_bit_1 -COL092_bit0 -COL092_bit1 -COL092_bit2 -COL092_bit3 -COL092_bit4 -COL092_bit5 -COL092_bit6 -COL092_bit7 -COL092_bit8 -COL092_bit9 -COL092_bit10 -COL092_bit11 -COL092_bit12 -COL092_bit13 -COL092_bit14 -COL092_bit15 -COL092_bit16 -COL092_bit17 -COL092_bit18 -COL092_bit19 -COL098_bit_10 -COL098_bit_9 -COL098_bit_8 -COL098_bit_7 -COL098_bit_6 -COL098_bit_5 -COL098_bit_4 -COL098_bit_3 -COL098_bit_2 -COL098_bit_1 -COL098_bit0 -COL098_bit1 -COL098_bit2 -COL098_bit3 -COL098_bit4 -COL098_bit5 -COL098_bit6 -COL098_bit7 -COL098_bit8 -COL098_bit9 -COL098_bit10 -COL098_bit11 -COL098_bit12 -COL098_bit13 -COL098_bit14 -COL098_bit15 -COL098_bit16 -COL098_bit17 -COL098_bit18 -COL098_bit19 -COL104_bit_10 -COL104_bit_9 -COL104_bit_8 -COL104_bit_7 -COL104_bit_6 -COL104_bit_5 -COL104_bit_4 -COL104_bit_3 -COL104_bit_2 -COL104_bit_1 -COL104_bit0 -COL104_bit1 -COL104_bit2 -COL104_bit3 -COL104_bit4 -COL104_bit5 -COL104_bit6 -COL104_bit7 -COL104_bit8 -COL104_bit9 -COL104_bit10 -COL104_bit11 -COL104_bit12 -COL104_bit13 -COL104_bit14 -COL104_bit15 -COL104_bit16 -COL104_bit17 -COL104_bit18 -COL104_bit19 -COL110_bit_10 -COL110_bit_9 -COL110_bit_8 -COL110_bit_7 -COL110_bit_6 -COL110_bit_5 -COL110_bit_4 -COL110_bit_3 -COL110_bit_2 -COL110_bit_1 -COL110_bit0 -COL110_bit1 -COL110_bit2 -COL110_bit3 -COL110_bit4 -COL110_bit5 -COL110_bit6 -COL110_bit7 -COL110_bit8 -COL110_bit9 -COL110_bit10 -COL110_bit11 -COL110_bit12 -COL110_bit13 -COL110_bit14 -COL110_bit15 -COL110_bit16 -COL110_bit17 -COL110_bit18 -COL110_bit19 -COL087_bit_10 -COL087_bit_9 -COL087_bit_8 -COL087_bit_7 -COL087_bit_6 -COL087_bit_5 -COL087_bit_4 -COL087_bit_3 -COL087_bit_2 -COL087_bit_1 -COL087_bit0 -COL087_bit1 -COL087_bit2 -COL087_bit3 -COL087_bit4 -COL087_bit5 -COL087_bit6 -COL087_bit7 -COL087_bit8 -COL087_bit9 -COL087_bit10 -COL087_bit11 -COL087_bit12 -COL087_bit13 -COL087_bit14 -COL087_bit15 -COL087_bit16 -COL087_bit17 -COL087_bit18 -COL087_bit19 -COL088_bit_10 -COL088_bit_9 -COL088_bit_8 -COL088_bit_7 -COL088_bit_6 -COL088_bit_5 -COL088_bit_4 -COL088_bit_3 -COL088_bit_2 -COL088_bit_1 -COL088_bit0 -COL088_bit1 -COL088_bit2 -COL088_bit3 -COL088_bit4 -COL088_bit5 -COL088_bit6 -COL088_bit7 -COL088_bit8 -COL088_bit9 -COL088_bit10 -COL088_bit11 -COL088_bit12 -COL088_bit13 -COL088_bit14 -COL088_bit15 -COL088_bit16 -COL088_bit17 -COL088_bit18 -COL088_bit19 -COL089_bit_10 -COL089_bit_9 -COL089_bit_8 -COL089_bit_7 -COL089_bit_6 -COL089_bit_5 -COL089_bit_4 -COL089_bit_3 -COL089_bit_2 -COL089_bit_1 -COL089_bit0 -COL089_bit1 -COL089_bit2 -COL089_bit3 -COL089_bit4 -COL089_bit5 -COL089_bit6 -COL089_bit7 -COL089_bit8 -COL089_bit9 -COL089_bit10 -COL089_bit11 -COL089_bit12 -COL089_bit13 -COL089_bit14 -COL089_bit15 -COL089_bit16 -COL089_bit17 -COL089_bit18 -COL089_bit19 -COL090_bit_10 -COL090_bit_9 -COL090_bit_8 -COL090_bit_7 -COL090_bit_6 -COL090_bit_5 -COL090_bit_4 -COL090_bit_3 -COL090_bit_2 -COL090_bit_1 -COL090_bit0 -COL090_bit1 -COL090_bit2 -COL090_bit3 -COL090_bit4 -COL090_bit5 -COL090_bit6 -COL090_bit7 -COL090_bit8 -COL090_bit9 -COL090_bit10 -COL090_bit11 -COL090_bit12 -COL090_bit13 -COL090_bit14 -COL090_bit15 -COL090_bit16 -COL090_bit17 -COL090_bit18 -COL090_bit19 -COL093_bit_10 -COL093_bit_9 -COL093_bit_8 -COL093_bit_7 -COL093_bit_6 -COL093_bit_5 -COL093_bit_4 -COL093_bit_3 -COL093_bit_2 -COL093_bit_1 -COL093_bit0 -COL093_bit1 -COL093_bit2 COL093_bit3 -COL093_bit4 -COL093_bit5 COL093_bit6 COL093_bit7 -COL093_bit8 -COL093_bit9 -COL093_bit10 -COL093_bit11 -COL093_bit12 -COL093_bit13 -COL093_bit14 -COL093_bit15 -COL093_bit16 -COL093_bit17 -COL093_bit18 -COL093_bit19 -COL099_bit_10 -COL099_bit_9 -COL099_bit_8 -COL099_bit_7 -COL099_bit_6 -COL099_bit_5 -COL099_bit_4 -COL099_bit_3 -COL099_bit_2 -COL099_bit_1 -COL099_bit0 -COL099_bit1 -COL099_bit2 -COL099_bit3 -COL099_bit4 -COL099_bit5 -COL099_bit6 -COL099_bit7 -COL099_bit8 -COL099_bit9 -COL099_bit10 -COL099_bit11 -COL099_bit12 -COL099_bit13 -COL099_bit14 -COL099_bit15 -COL099_bit16 -COL099_bit17 -COL099_bit18 -COL099_bit19 -COL105_bit_10 -COL105_bit_9 -COL105_bit_8 -COL105_bit_7 -COL105_bit_6 -COL105_bit_5 -COL105_bit_4 -COL105_bit_3 -COL105_bit_2 -COL105_bit_1 -COL105_bit0 -COL105_bit1 -COL105_bit2 -COL105_bit3 -COL105_bit4 -COL105_bit5 -COL105_bit6 -COL105_bit7 -COL105_bit8 -COL105_bit9 -COL105_bit10 -COL105_bit11 -COL105_bit12 -COL105_bit13 -COL105_bit14 -COL105_bit15 -COL105_bit16 -COL105_bit17 -COL105_bit18 -COL105_bit19 -COL111_bit_10 -COL111_bit_9 -COL111_bit_8 -COL111_bit_7 -COL111_bit_6 -COL111_bit_5 -COL111_bit_4 -COL111_bit_3 -COL111_bit_2 -COL111_bit_1 -COL111_bit0 -COL111_bit1 -COL111_bit2 -COL111_bit3 -COL111_bit4 -COL111_bit5 -COL111_bit6 -COL111_bit7 -COL111_bit8 -COL111_bit9 -COL111_bit10 -COL111_bit11 -COL111_bit12 -COL111_bit13 -COL111_bit14 -COL111_bit15 -COL111_bit16 -COL111_bit17 -COL111_bit18 -COL111_bit19 -COL094_bit_10 -COL094_bit_9 -COL094_bit_8 -COL094_bit_7 -COL094_bit_6 -COL094_bit_5 -COL094_bit_4 -COL094_bit_3 -COL094_bit_2 -COL094_bit_1 -COL094_bit0 -COL094_bit1 -COL094_bit2 -COL094_bit3 -COL094_bit4 -COL094_bit5 -COL094_bit6 -COL094_bit7 -COL094_bit8 -COL094_bit9 -COL094_bit10 -COL094_bit11 -COL094_bit12 -COL094_bit13 -COL094_bit14 -COL094_bit15 -COL094_bit16 -COL094_bit17 -COL094_bit18 -COL094_bit19 -COL095_bit_10 -COL095_bit_9 -COL095_bit_8 -COL095_bit_7 -COL095_bit_6 -COL095_bit_5 -COL095_bit_4 -COL095_bit_3 -COL095_bit_2 -COL095_bit_1 -COL095_bit0 -COL095_bit1 -COL095_bit2 -COL095_bit3 -COL095_bit4 -COL095_bit5 -COL095_bit6 -COL095_bit7 -COL095_bit8 -COL095_bit9 -COL095_bit10 -COL095_bit11 -COL095_bit12 -COL095_bit13 -COL095_bit14 -COL095_bit15 -COL095_bit16 -COL095_bit17 -COL095_bit18 -COL095_bit19 -COL096_bit_10 -COL096_bit_9 -COL096_bit_8 -COL096_bit_7 -COL096_bit_6 -COL096_bit_5 -COL096_bit_4 -COL096_bit_3 -COL096_bit_2 -COL096_bit_1 -COL096_bit0 -COL096_bit1 -COL096_bit2 -COL096_bit3 -COL096_bit4 -COL096_bit5 -COL096_bit6 -COL096_bit7 -COL096_bit8 -COL096_bit9 -COL096_bit10 -COL096_bit11 -COL096_bit12 -COL096_bit13 -COL096_bit14 -COL096_bit15 -COL096_bit16 -COL096_bit17 -COL096_bit18 -COL096_bit19 -COL100_bit_10 -COL100_bit_9 -COL100_bit_8 -COL100_bit_7 -COL100_bit_6 -COL100_bit_5 -COL100_bit_4 -COL100_bit_3 -COL100_bit_2 -COL100_bit_1 -COL100_bit0 -COL100_bit1 -COL100_bit2 -COL100_bit3 -COL100_bit4 -COL100_bit5 -COL100_bit6 -COL100_bit7 -COL100_bit8 -COL100_bit9 -COL100_bit10 -COL100_bit11 -COL100_bit12 -COL100_bit13 -COL100_bit14 -COL100_bit15 -COL100_bit16 -COL100_bit17 -COL100_bit18 -COL100_bit19 -COL106_bit_10 -COL106_bit_9 -COL106_bit_8 -COL106_bit_7 -COL106_bit_6 -COL106_bit_5 -COL106_bit_4 -COL106_bit_3 -COL106_bit_2 -COL106_bit_1 -COL106_bit0 -COL106_bit1 -COL106_bit2 -COL106_bit3 -COL106_bit4 -COL106_bit5 -COL106_bit6 -COL106_bit7 -COL106_bit8 -COL106_bit9 -COL106_bit10 -COL106_bit11 -COL106_bit12 -COL106_bit13 -COL106_bit14 -COL106_bit15 -COL106_bit16 -COL106_bit17 -COL106_bit18 -COL106_bit19 -COL112_bit_10 -COL112_bit_9 -COL112_bit_8 -COL112_bit_7 -COL112_bit_6 -COL112_bit_5 -COL112_bit_4 -COL112_bit_3 -COL112_bit_2 -COL112_bit_1 -COL112_bit0 -COL112_bit1 -COL112_bit2 -COL112_bit3 -COL112_bit4 -COL112_bit5 -COL112_bit6 -COL112_bit7 -COL112_bit8 -COL112_bit9 -COL112_bit10 -COL112_bit11 -COL112_bit12 -COL112_bit13 -COL112_bit14 -COL112_bit15 -COL112_bit16 -COL112_bit17 -COL112_bit18 -COL112_bit19 -COL101_bit_10 -COL101_bit_9 -COL101_bit_8 -COL101_bit_7 -COL101_bit_6 -COL101_bit_5 -COL101_bit_4 -COL101_bit_3 -COL101_bit_2 -COL101_bit_1 -COL101_bit0 COL101_bit1 COL101_bit2 COL101_bit3 COL101_bit4 -COL101_bit5 -COL101_bit6 -COL101_bit7 -COL101_bit8 -COL101_bit9 -COL101_bit10 -COL101_bit11 -COL101_bit12 -COL101_bit13 -COL101_bit14 -COL101_bit15 -COL101_bit16 -COL101_bit17 -COL101_bit18 -COL101_bit19 -COL102_bit_10 -COL102_bit_9 -COL102_bit_8 -COL102_bit_7 -COL102_bit_6 -COL102_bit_5 -COL102_bit_4 -COL102_bit_3 -COL102_bit_2 -COL102_bit_1 -COL102_bit0 -COL102_bit1 -COL102_bit2 -COL102_bit3 -COL102_bit4 -COL102_bit5 -COL102_bit6 -COL102_bit7 -COL102_bit8 -COL102_bit9 -COL102_bit10 -COL102_bit11 -COL102_bit12 -COL102_bit13 -COL102_bit14 -COL102_bit15 -COL102_bit16 -COL102_bit17 -COL102_bit18 -COL102_bit19 -COL107_bit_10 -COL107_bit_9 -COL107_bit_8 -COL107_bit_7 -COL107_bit_6 -COL107_bit_5 -COL107_bit_4 -COL107_bit_3 -COL107_bit_2 -COL107_bit_1 -COL107_bit0 -COL107_bit1 -COL107_bit2 -COL107_bit3 -COL107_bit4 -COL107_bit5 -COL107_bit6 -COL107_bit7 -COL107_bit8 -COL107_bit9 -COL107_bit10 -COL107_bit11 -COL107_bit12 -COL107_bit13 -COL107_bit14 -COL107_bit15 -COL107_bit16 -COL107_bit17 -COL107_bit18 -COL107_bit19 -COL113_bit_10 -COL113_bit_9 -COL113_bit_8 -COL113_bit_7 -COL113_bit_6 -COL113_bit_5 -COL113_bit_4 -COL113_bit_3 -COL113_bit_2 -COL113_bit_1 -COL113_bit0 -COL113_bit1 -COL113_bit2 -COL113_bit3 -COL113_bit4 -COL113_bit5 -COL113_bit6 -COL113_bit7 -COL113_bit8 -COL113_bit9 -COL113_bit10 -COL113_bit11 -COL113_bit12 -COL113_bit13 -COL113_bit14 -COL113_bit15 -COL113_bit16 -COL113_bit17 -COL113_bit18 -COL113_bit19 -COL108_bit_10 -COL108_bit_9 -COL108_bit_8 -COL108_bit_7 -COL108_bit_6 -COL108_bit_5 -COL108_bit_4 -COL108_bit_3 -COL108_bit_2 -COL108_bit_1 -COL108_bit0 -COL108_bit1 -COL108_bit2 -COL108_bit3 -COL108_bit4 -COL108_bit5 -COL108_bit6 -COL108_bit7 -COL108_bit8 -COL108_bit9 -COL108_bit10 -COL108_bit11 -COL108_bit12 -COL108_bit13 -COL108_bit14 -COL108_bit15 -COL108_bit16 -COL108_bit17 -COL108_bit18 -COL108_bit19 -COL114_bit_10 -COL114_bit_9 -COL114_bit_8 -COL114_bit_7 -COL114_bit_6 -COL114_bit_5 -COL114_bit_4 -COL114_bit_3 -COL114_bit_2 -COL114_bit_1 -COL114_bit0 -COL114_bit1 -COL114_bit2 -COL114_bit3 -COL114_bit4 -COL114_bit5 -COL114_bit6 -COL114_bit7 -COL114_bit8 -COL114_bit9 -COL114_bit10 -COL114_bit11 -COL114_bit12 -COL114_bit13 -COL114_bit14 -COL114_bit15 -COL114_bit16 -COL114_bit17 -COL114_bit18 -COL114_bit19 -COL131_bit_10 -COL131_bit_9 -COL131_bit_8 -COL131_bit_7 -COL131_bit_6 -COL131_bit_5 -COL131_bit_4 -COL131_bit_3 -COL131_bit_2 -COL131_bit_1 COL131_bit0 -COL131_bit1 -COL131_bit2 -COL131_bit3 -COL131_bit4 -COL131_bit5 -COL131_bit6 -COL131_bit7 -COL131_bit8 -COL131_bit9 -COL131_bit10 -COL131_bit11 -COL131_bit12 -COL131_bit13 -COL131_bit14 -COL131_bit15 -COL131_bit16 -COL131_bit17 -COL131_bit18 -COL131_bit19 COL131_bit20 -COL132_bit_10 -COL132_bit_9 -COL132_bit_8 -COL132_bit_7 -COL132_bit_6 -COL132_bit_5 -COL132_bit_4 -COL132_bit_3 -COL132_bit_2 -COL132_bit_1 COL132_bit0 -COL132_bit1 -COL132_bit2 -COL132_bit3 -COL132_bit4 -COL132_bit5 -COL132_bit6 -COL132_bit7 -COL132_bit8 -COL132_bit9 -COL132_bit10 -COL132_bit11 -COL132_bit12 -COL132_bit13 -COL132_bit14 -COL132_bit15 -COL132_bit16 -COL132_bit17 -COL132_bit18 -COL132_bit19 COL132_bit20 c _______________________________________________________________________________ c c restarts : 97 c conflicts : 164435 (170 /sec) c decisions : 316278 (327 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 967.891 s c _______________________________________________________________________________
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/22177/stat): 22177 (minisat+_script) R 22176 22177 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846527801 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/22177/statm): 174 3 169 147 0 27 0 [pid=22177] 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=22178 New process pid=22179 New process pid=22180 execve syscall for /bin/sed executable One traced child (pid=22179) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=22180) exited with status: 0 One traced child (pid=22178) exited with status: 0 New process pid=22181 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-misc05.opb [startup+10.0041 s] Raw data (loadavg): 0.98 1.04 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 1877 0 0 0 977 8 0 0 25 0 1 0 1846527806 8241152 1861 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22181/statm): 2012 1861 145 145 0 1867 0 [pid=22181] vsize: 8048 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 10172 [startup+20.0059 s] Raw data (loadavg): 0.98 1.04 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 2160 0 0 0 1970 11 0 0 25 0 1 0 1846527806 9416704 2144 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22181/statm): 2299 2144 145 145 0 2154 0 [pid=22181] vsize: 9196 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 11320 [startup+30.0067 s] Raw data (loadavg): 0.98 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 2341 0 0 0 2966 13 0 0 25 0 1 0 1846527806 10141696 2325 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 2476 2325 145 145 0 2331 0 [pid=22181] vsize: 9904 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 12028 [startup+40.0075 s] Raw data (loadavg): 0.99 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 2672 0 0 0 3962 15 0 0 25 0 1 0 1846527806 11554816 2656 4294967295 134512640 135094434 3221224432 3221223056 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 2821 2656 145 145 0 2676 0 [pid=22181] vsize: 11284 Current children cumulated CPU time (s) 39.78 Current children cumulated vsize (Kb) 13408 [startup+50.0083 s] Raw data (loadavg): 0.99 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 2886 0 0 0 4958 17 0 0 25 0 1 0 1846527806 12419072 2870 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 3032 2870 145 145 0 2887 0 [pid=22181] vsize: 12128 Current children cumulated CPU time (s) 49.76 Current children cumulated vsize (Kb) 14252 [startup+60.0091 s] Raw data (loadavg): 0.99 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 2906 0 0 0 5957 17 0 0 25 0 1 0 1846527806 12496896 2890 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 3051 2890 145 145 0 2906 0 [pid=22181] vsize: 12204 Current children cumulated CPU time (s) 59.75 Current children cumulated vsize (Kb) 14328 [startup+70.01 s] Raw data (loadavg): 0.99 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 2906 0 0 0 6957 18 0 0 25 0 1 0 1846527806 12496896 2890 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 3051 2890 145 145 0 2906 0 [pid=22181] vsize: 12204 Current children cumulated CPU time (s) 69.76 Current children cumulated vsize (Kb) 14328 [startup+80.0108 s] Raw data (loadavg): 0.99 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 3092 0 0 0 7954 18 0 0 25 0 1 0 1846527806 13262848 3076 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 3238 3076 145 145 0 3093 0 [pid=22181] vsize: 12952 Current children cumulated CPU time (s) 79.73 Current children cumulated vsize (Kb) 15076 [startup+90.0116 s] Raw data (loadavg): 0.99 1.03 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 3390 0 0 0 8949 20 0 0 25 0 1 0 1846527806 14467072 3374 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 3532 3374 145 145 0 3387 0 [pid=22181] vsize: 14128 Current children cumulated CPU time (s) 89.7 Current children cumulated vsize (Kb) 16252 [startup+100.012 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 3662 0 0 0 9945 22 0 0 25 0 1 0 1846527806 15572992 3646 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 3802 3646 145 145 0 3657 0 [pid=22181] vsize: 15208 Current children cumulated CPU time (s) 99.68 Current children cumulated vsize (Kb) 17332 [startup+110.014 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4082 0 0 0 10941 25 0 0 25 0 1 0 1846527806 17281024 4066 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 4219 4066 145 145 0 4074 0 [pid=22181] vsize: 16876 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 19000 [startup+120.015 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4447 0 0 0 11936 28 0 0 25 0 1 0 1846527806 18767872 4431 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 4582 4431 145 145 0 4437 0 [pid=22181] vsize: 18328 Current children cumulated CPU time (s) 119.65 Current children cumulated vsize (Kb) 20452 [startup+130.016 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4787 0 0 0 12932 30 0 0 25 0 1 0 1846527806 20152320 4771 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 4920 4771 145 145 0 4775 0 [pid=22181] vsize: 19680 Current children cumulated CPU time (s) 129.63 Current children cumulated vsize (Kb) 21804 [startup+140.017 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4787 0 0 0 13932 30 0 0 25 0 1 0 1846527806 20152320 4771 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 4920 4771 145 145 0 4775 0 [pid=22181] vsize: 19680 Current children cumulated CPU time (s) 139.63 Current children cumulated vsize (Kb) 21804 [startup+150.017 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4787 0 0 0 14932 30 0 0 25 0 1 0 1846527806 20152320 4771 4294967295 134512640 135094434 3221224432 3221223056 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 4920 4771 145 145 0 4775 0 [pid=22181] vsize: 19680 Current children cumulated CPU time (s) 149.63 Current children cumulated vsize (Kb) 21804 [startup+160.018 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4787 0 0 0 15932 30 0 0 25 0 1 0 1846527806 20152320 4771 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 4920 4771 145 145 0 4775 0 [pid=22181] vsize: 19680 Current children cumulated CPU time (s) 159.63 Current children cumulated vsize (Kb) 21804 [startup+170.019 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 4917 0 0 0 16931 30 0 0 25 0 1 0 1846527806 20692992 4901 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5052 4901 145 145 0 4907 0 [pid=22181] vsize: 20208 Current children cumulated CPU time (s) 169.62 Current children cumulated vsize (Kb) 22332 [startup+180.02 s] Raw data (loadavg): 0.99 1.02 1.00 1/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) T 22177 22177 5929 0 -1 0 5207 0 0 0 17926 32 0 0 25 0 1 0 1846527806 21876736 5191 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5341 5191 145 145 0 5196 0 [pid=22181] vsize: 21364 Current children cumulated CPU time (s) 179.59 Current children cumulated vsize (Kb) 23488 [startup+190.022 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5431 0 0 0 18923 34 0 0 25 0 1 0 1846527806 22790144 5415 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5415 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 189.58 Current children cumulated vsize (Kb) 24380 [startup+200.023 s] Raw data (loadavg): 0.99 1.02 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5431 0 0 0 19924 34 0 0 25 0 1 0 1846527806 22790144 5415 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5415 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 199.59 Current children cumulated vsize (Kb) 24380 [startup+210.023 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5431 0 0 0 20924 34 0 0 25 0 1 0 1846527806 22790144 5415 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5415 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 209.59 Current children cumulated vsize (Kb) 24380 [startup+220.026 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5431 0 0 0 21924 34 0 0 25 0 1 0 1846527806 22790144 5415 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5415 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 219.59 Current children cumulated vsize (Kb) 24380 [startup+230.026 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5431 0 0 0 22924 34 0 0 25 0 1 0 1846527806 22790144 5415 4294967295 134512640 135094434 3221224432 3221223104 134556587 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5415 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 229.59 Current children cumulated vsize (Kb) 24380 [startup+240.027 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5432 0 0 0 23924 34 0 0 25 0 1 0 1846527806 22790144 5416 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5416 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 239.59 Current children cumulated vsize (Kb) 24380 [startup+250.028 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5432 0 0 0 24925 34 0 0 25 0 1 0 1846527806 22790144 5416 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5416 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 249.6 Current children cumulated vsize (Kb) 24380 [startup+260.028 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5432 0 0 0 25925 34 0 0 25 0 1 0 1846527806 22790144 5416 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5564 5416 145 145 0 5419 0 [pid=22181] vsize: 22256 Current children cumulated CPU time (s) 259.6 Current children cumulated vsize (Kb) 24380 [startup+270.029 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 26923 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 269.59 Current children cumulated vsize (Kb) 25252 [startup+280.03 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 27923 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 279.59 Current children cumulated vsize (Kb) 25252 [startup+290.031 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 28923 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 289.59 Current children cumulated vsize (Kb) 25252 [startup+300.032 s] Raw data (loadavg): 0.99 1.01 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 29923 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 299.59 Current children cumulated vsize (Kb) 25252 [startup+310.033 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 30923 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 309.59 Current children cumulated vsize (Kb) 25252 [startup+320.034 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 31924 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 319.6 Current children cumulated vsize (Kb) 25252 [startup+330.035 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 32924 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 329.6 Current children cumulated vsize (Kb) 25252 [startup+340.036 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5650 0 0 0 33924 35 0 0 25 0 1 0 1846527806 23683072 5634 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5782 5634 145 145 0 5637 0 [pid=22181] vsize: 23128 Current children cumulated CPU time (s) 339.6 Current children cumulated vsize (Kb) 25252 [startup+350.037 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5747 0 0 0 34923 36 0 0 25 0 1 0 1846527806 24080384 5731 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 5879 5731 145 145 0 5734 0 [pid=22181] vsize: 23516 Current children cumulated CPU time (s) 349.6 Current children cumulated vsize (Kb) 25640 [startup+360.038 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 5999 0 0 0 35919 37 0 0 25 0 1 0 1846527806 25124864 5983 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 6134 5983 145 145 0 5989 0 [pid=22181] vsize: 24536 Current children cumulated CPU time (s) 359.57 Current children cumulated vsize (Kb) 26660 [startup+370.038 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 6210 0 0 0 36917 39 0 0 25 0 1 0 1846527806 25993216 6194 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 6346 6194 145 145 0 6201 0 [pid=22181] vsize: 25384 Current children cumulated CPU time (s) 369.57 Current children cumulated vsize (Kb) 27508 [startup+380.038 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 6447 0 0 0 37914 39 0 0 25 0 1 0 1846527806 26984448 6431 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 6588 6431 145 145 0 6443 0 [pid=22181] vsize: 26352 Current children cumulated CPU time (s) 379.54 Current children cumulated vsize (Kb) 28476 [startup+390.04 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 6707 0 0 0 38911 41 0 0 25 0 1 0 1846527806 28086272 6691 4294967295 134512640 135094434 3221224432 3221223024 134557271 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 6857 6691 145 145 0 6712 0 [pid=22181] vsize: 27428 Current children cumulated CPU time (s) 389.53 Current children cumulated vsize (Kb) 29552 [startup+400.041 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 6986 0 0 0 39908 43 0 0 25 0 1 0 1846527806 29392896 6970 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 7176 6970 145 145 0 7031 0 [pid=22181] vsize: 28704 Current children cumulated CPU time (s) 399.52 Current children cumulated vsize (Kb) 30828 [startup+410.042 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 7280 0 0 0 40905 44 0 0 25 0 1 0 1846527806 30613504 7264 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 7474 7264 145 145 0 7329 0 [pid=22181] vsize: 29896 Current children cumulated CPU time (s) 409.5 Current children cumulated vsize (Kb) 32020 [startup+420.042 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 7433 0 0 0 41903 45 0 0 25 0 1 0 1846527806 31248384 7417 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 7629 7417 145 145 0 7484 0 [pid=22181] vsize: 30516 Current children cumulated CPU time (s) 419.49 Current children cumulated vsize (Kb) 32640 [startup+430.043 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 7520 0 0 0 42902 45 0 0 25 0 1 0 1846527806 31645696 7504 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 7726 7504 145 145 0 7581 0 [pid=22181] vsize: 30904 Current children cumulated CPU time (s) 429.48 Current children cumulated vsize (Kb) 33028 [startup+440.044 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 7738 0 0 0 43900 46 0 0 25 0 1 0 1846527806 32538624 7722 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 7944 7722 145 145 0 7799 0 [pid=22181] vsize: 31776 Current children cumulated CPU time (s) 439.47 Current children cumulated vsize (Kb) 33900 [startup+450.045 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 8062 0 0 0 44897 48 0 0 25 0 1 0 1846527806 33886208 8046 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 8273 8046 145 145 0 8128 0 [pid=22181] vsize: 33092 Current children cumulated CPU time (s) 449.46 Current children cumulated vsize (Kb) 35216 [startup+460.047 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 8355 0 0 0 45895 49 0 0 25 0 1 0 1846527806 35069952 8339 4294967295 134512640 135094434 3221224432 3221223056 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 8562 8339 145 145 0 8417 0 [pid=22181] vsize: 34248 Current children cumulated CPU time (s) 459.45 Current children cumulated vsize (Kb) 36372 [startup+470.047 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 8648 0 0 0 46891 50 0 0 25 0 1 0 1846527806 36257792 8632 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 8852 8632 145 145 0 8707 0 [pid=22181] vsize: 35408 Current children cumulated CPU time (s) 469.42 Current children cumulated vsize (Kb) 37532 [startup+480.048 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 8910 0 0 0 47887 53 0 0 25 0 1 0 1846527806 37306368 8894 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 9108 8894 145 145 0 8963 0 [pid=22181] vsize: 36432 Current children cumulated CPU time (s) 479.41 Current children cumulated vsize (Kb) 38556 [startup+490.05 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 9230 0 0 0 48885 54 0 0 25 0 1 0 1846527806 38612992 9214 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 9427 9214 145 145 0 9282 0 [pid=22181] vsize: 37708 Current children cumulated CPU time (s) 489.4 Current children cumulated vsize (Kb) 39832 [startup+500.051 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 9497 0 0 0 49882 56 0 0 25 0 1 0 1846527806 39690240 9481 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 9690 9481 145 145 0 9545 0 [pid=22181] vsize: 38760 Current children cumulated CPU time (s) 499.39 Current children cumulated vsize (Kb) 40884 [startup+510.052 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 9791 0 0 0 50879 58 0 0 25 0 1 0 1846527806 40894464 9775 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 9984 9775 145 145 0 9839 0 [pid=22181] vsize: 39936 Current children cumulated CPU time (s) 509.38 Current children cumulated vsize (Kb) 42060 [startup+520.053 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 10079 0 0 0 51877 59 0 0 25 0 1 0 1846527806 42070016 10063 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 10271 10063 145 145 0 10126 0 [pid=22181] vsize: 41084 Current children cumulated CPU time (s) 519.37 Current children cumulated vsize (Kb) 43208 [startup+530.052 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 10268 0 0 0 52876 59 0 0 25 0 1 0 1846527806 42831872 10252 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 10457 10252 145 145 0 10312 0 [pid=22181] vsize: 41828 Current children cumulated CPU time (s) 529.36 Current children cumulated vsize (Kb) 43952 [startup+540.053 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) T 22177 22177 5929 0 -1 0 10551 0 0 0 53873 61 0 0 25 0 1 0 1846527806 43974656 10535 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22181/statm): 10736 10535 145 145 0 10591 0 [pid=22181] vsize: 42944 Current children cumulated CPU time (s) 539.35 Current children cumulated vsize (Kb) 45068 [startup+550.054 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 10820 0 0 0 54870 63 0 0 25 0 1 0 1846527806 45088768 10804 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 11008 10804 145 145 0 10863 0 [pid=22181] vsize: 44032 Current children cumulated CPU time (s) 549.34 Current children cumulated vsize (Kb) 46156 [startup+560.056 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 11159 0 0 0 55866 65 0 0 25 0 1 0 1846527806 46477312 11143 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 11347 11143 145 145 0 11202 0 [pid=22181] vsize: 45388 Current children cumulated CPU time (s) 559.32 Current children cumulated vsize (Kb) 47512 [startup+570.057 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 11457 0 0 0 56862 67 0 0 25 0 1 0 1846527806 47689728 11441 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 11643 11441 145 145 0 11498 0 [pid=22181] vsize: 46572 Current children cumulated CPU time (s) 569.3 Current children cumulated vsize (Kb) 48696 [startup+580.057 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 11754 0 0 0 57859 68 0 0 25 0 1 0 1846527806 48918528 11738 4294967295 134512640 135094434 3221224432 3221223084 134556676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 11943 11738 145 145 0 11798 0 [pid=22181] vsize: 47772 Current children cumulated CPU time (s) 579.28 Current children cumulated vsize (Kb) 49896 [startup+590.058 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12037 0 0 0 58856 70 0 0 25 0 1 0 1846527806 50049024 12021 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 12219 12021 145 145 0 12074 0 [pid=22181] vsize: 48876 Current children cumulated CPU time (s) 589.27 Current children cumulated vsize (Kb) 51000 [startup+600.059 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12311 0 0 0 59853 71 0 0 25 0 1 0 1846527806 51228672 12295 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 12507 12295 145 145 0 12362 0 [pid=22181] vsize: 50028 Current children cumulated CPU time (s) 599.25 Current children cumulated vsize (Kb) 52152 [startup+610.06 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12562 0 0 0 60851 72 0 0 25 0 1 0 1846527806 52310016 12546 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 12771 12546 145 145 0 12626 0 [pid=22181] vsize: 51084 Current children cumulated CPU time (s) 609.24 Current children cumulated vsize (Kb) 53208 [startup+620.061 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12828 0 0 0 61849 73 0 0 25 0 1 0 1846527806 53452800 12812 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13050 12812 145 145 0 12905 0 [pid=22181] vsize: 52200 Current children cumulated CPU time (s) 619.23 Current children cumulated vsize (Kb) 54324 [startup+630.061 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12853 0 0 0 62849 73 0 0 25 0 1 0 1846527806 53547008 12837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13073 12837 145 145 0 12928 0 [pid=22181] vsize: 52292 Current children cumulated CPU time (s) 629.23 Current children cumulated vsize (Kb) 54416 [startup+640.063 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12853 0 0 0 63849 73 0 0 25 0 1 0 1846527806 53547008 12837 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13073 12837 145 145 0 12928 0 [pid=22181] vsize: 52292 Current children cumulated CPU time (s) 639.23 Current children cumulated vsize (Kb) 54416 [startup+650.064 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12853 0 0 0 64850 73 0 0 25 0 1 0 1846527806 53547008 12837 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13073 12837 145 145 0 12928 0 [pid=22181] vsize: 52292 Current children cumulated CPU time (s) 649.24 Current children cumulated vsize (Kb) 54416 [startup+660.066 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12853 0 0 0 65850 73 0 0 25 0 1 0 1846527806 53547008 12837 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13073 12837 145 145 0 12928 0 [pid=22181] vsize: 52292 Current children cumulated CPU time (s) 659.24 Current children cumulated vsize (Kb) 54416 [startup+670.067 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12853 0 0 0 66850 73 0 0 25 0 1 0 1846527806 53547008 12837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13073 12837 145 145 0 12928 0 [pid=22181] vsize: 52292 Current children cumulated CPU time (s) 669.24 Current children cumulated vsize (Kb) 54416 [startup+680.067 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12855 0 0 0 67850 73 0 0 25 0 1 0 1846527806 53547008 12839 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13073 12839 145 145 0 12928 0 [pid=22181] vsize: 52292 Current children cumulated CPU time (s) 679.24 Current children cumulated vsize (Kb) 54416 [startup+690.067 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12865 0 0 0 68850 73 0 0 25 0 1 0 1846527806 53612544 12849 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22181/statm): 13089 12849 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 689.24 Current children cumulated vsize (Kb) 54480 [startup+700.069 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12865 0 0 0 69850 73 0 0 25 0 1 0 1846527806 53612544 12849 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12849 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 699.24 Current children cumulated vsize (Kb) 54480 [startup+710.07 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12865 0 0 0 70850 73 0 0 25 0 1 0 1846527806 53612544 12849 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12849 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 709.24 Current children cumulated vsize (Kb) 54480 [startup+720.071 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12865 0 0 0 71851 73 0 0 25 0 1 0 1846527806 53612544 12849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12849 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 719.25 Current children cumulated vsize (Kb) 54480 [startup+730.072 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12866 0 0 0 72851 73 0 0 25 0 1 0 1846527806 53612544 12850 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12850 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 729.25 Current children cumulated vsize (Kb) 54480 [startup+740.072 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12866 0 0 0 73851 73 0 0 25 0 1 0 1846527806 53612544 12850 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12850 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 739.25 Current children cumulated vsize (Kb) 54480 [startup+750.073 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12867 0 0 0 74851 73 0 0 25 0 1 0 1846527806 53612544 12851 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12851 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 749.25 Current children cumulated vsize (Kb) 54480 [startup+760.075 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12868 0 0 0 75852 73 0 0 25 0 1 0 1846527806 53612544 12852 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12852 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 759.26 Current children cumulated vsize (Kb) 54480 [startup+770.076 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12874 0 0 0 76852 73 0 0 25 0 1 0 1846527806 53612544 12858 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12858 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 769.26 Current children cumulated vsize (Kb) 54480 [startup+780.077 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12875 0 0 0 77852 73 0 0 25 0 1 0 1846527806 53612544 12859 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12859 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 779.26 Current children cumulated vsize (Kb) 54480 [startup+790.077 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12877 0 0 0 78852 73 0 0 25 0 1 0 1846527806 53612544 12861 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13089 12861 145 145 0 12944 0 [pid=22181] vsize: 52356 Current children cumulated CPU time (s) 789.26 Current children cumulated vsize (Kb) 54480 [startup+800.078 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12896 0 0 0 79852 73 0 0 25 0 1 0 1846527806 53743616 12880 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13121 12880 145 145 0 12976 0 [pid=22181] vsize: 52484 Current children cumulated CPU time (s) 799.26 Current children cumulated vsize (Kb) 54608 [startup+810.08 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12900 0 0 0 80853 73 0 0 25 0 1 0 1846527806 53743616 12884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13121 12884 145 145 0 12976 0 [pid=22181] vsize: 52484 Current children cumulated CPU time (s) 809.27 Current children cumulated vsize (Kb) 54608 [startup+820.081 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12920 0 0 0 81853 74 0 0 25 0 1 0 1846527806 53874688 12904 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13153 12904 145 145 0 13008 0 [pid=22181] vsize: 52612 Current children cumulated CPU time (s) 819.28 Current children cumulated vsize (Kb) 54736 [startup+830.082 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12921 0 0 0 82853 74 0 0 25 0 1 0 1846527806 53874688 12905 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13153 12905 145 145 0 13008 0 [pid=22181] vsize: 52612 Current children cumulated CPU time (s) 829.28 Current children cumulated vsize (Kb) 54736 [startup+840.082 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12921 0 0 0 83853 74 0 0 25 0 1 0 1846527806 53874688 12905 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13153 12905 145 145 0 13008 0 [pid=22181] vsize: 52612 Current children cumulated CPU time (s) 839.28 Current children cumulated vsize (Kb) 54736 [startup+850.083 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12922 0 0 0 84854 74 0 0 25 0 1 0 1846527806 53874688 12906 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13153 12906 145 145 0 13008 0 [pid=22181] vsize: 52612 Current children cumulated CPU time (s) 849.29 Current children cumulated vsize (Kb) 54736 [startup+860.085 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12922 0 0 0 85854 74 0 0 25 0 1 0 1846527806 53874688 12906 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13153 12906 145 145 0 13008 0 [pid=22181] vsize: 52612 Current children cumulated CPU time (s) 859.29 Current children cumulated vsize (Kb) 54736 [startup+870.086 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12944 0 0 0 86854 74 0 0 25 0 1 0 1846527806 54005760 12928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13185 12928 145 145 0 13040 0 [pid=22181] vsize: 52740 Current children cumulated CPU time (s) 869.29 Current children cumulated vsize (Kb) 54864 [startup+880.086 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12947 0 0 0 87854 74 0 0 25 0 1 0 1846527806 54005760 12931 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13185 12931 145 145 0 13040 0 [pid=22181] vsize: 52740 Current children cumulated CPU time (s) 879.29 Current children cumulated vsize (Kb) 54864 [startup+890.087 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12947 0 0 0 88854 74 0 0 25 0 1 0 1846527806 54005760 12931 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13185 12931 145 145 0 13040 0 [pid=22181] vsize: 52740 Current children cumulated CPU time (s) 889.29 Current children cumulated vsize (Kb) 54864 [startup+900.087 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12969 0 0 0 89854 74 0 0 25 0 1 0 1846527806 54136832 12953 4294967295 134512640 135094434 3221224432 3221223104 134556415 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13217 12953 145 145 0 13072 0 [pid=22181] vsize: 52868 Current children cumulated CPU time (s) 899.29 Current children cumulated vsize (Kb) 54992 [startup+910.088 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12972 0 0 0 90854 74 0 0 25 0 1 0 1846527806 54136832 12956 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22181/statm): 13217 12956 145 145 0 13072 0 [pid=22181] vsize: 52868 Current children cumulated CPU time (s) 909.29 Current children cumulated vsize (Kb) 54992 [startup+920.089 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12991 0 0 0 91853 74 0 0 25 0 1 0 1846527806 54530048 12975 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13313 12975 145 145 0 13168 0 [pid=22181] vsize: 53252 Current children cumulated CPU time (s) 919.28 Current children cumulated vsize (Kb) 55376 [startup+930.09 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 12994 0 0 0 92854 74 0 0 25 0 1 0 1846527806 54530048 12978 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13313 12978 145 145 0 13168 0 [pid=22181] vsize: 53252 Current children cumulated CPU time (s) 929.29 Current children cumulated vsize (Kb) 55376 [startup+940.091 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 13185 0 0 0 93852 75 0 0 25 0 1 0 1846527806 55304192 13169 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13502 13169 145 145 0 13357 0 [pid=22181] vsize: 54008 Current children cumulated CPU time (s) 939.28 Current children cumulated vsize (Kb) 56132 [startup+950.091 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 13325 0 0 0 94850 76 0 0 25 0 1 0 1846527806 55881728 13309 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13643 13309 145 145 0 13498 0 [pid=22181] vsize: 54572 Current children cumulated CPU time (s) 949.27 Current children cumulated vsize (Kb) 56696 [startup+960.092 s] Raw data (loadavg): 0.99 1.00 1.00 2/57 22181 Raw data (/proc/22177/stat): 22177 (minisat+_script) S 22176 22177 5929 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846527801 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22177/statm): 531 226 485 147 0 384 0 [pid=22177] vsize: 2124 Raw data (/proc/22181/stat): 22181 (minisat+_64-bit) R 22177 22177 5929 0 -1 0 13509 0 0 0 95849 78 0 0 25 0 1 0 1846527806 56623104 13493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22181/statm): 13824 13493 145 145 0 13679 0 [pid=22181] vsize: 55296 Current children cumulated CPU time (s) 959.28 Current children cumulated vsize (Kb) 57420 One traced child (pid=22181) exited with status: 30 One traced child (pid=22177) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 969.548 CPU time (s): 968.747 CPU user time (s): 967.913 CPU system time (s): 0.833873 CPU usage (%): 99.9173 Max. virtual memory (cumulated for all children) (Kb): 57420
Verifier: OK 1076796928