Name | normalized-opb/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 | NO |
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 | SAT |
Best CPU time to get the best result obtained on this benchmark | 952.576 |
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 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-05-25 18:46:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22107 boxname=wulflinc29 idbench=923 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 5e97a4ad772c87cdf15a611dd5b54048 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-misc05.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-misc05.opb IDLAUNCH: 22107 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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: 451768 kB Buffers: 35300 kB Cached: 522544 kB SwapCached: 572 kB Active: 66392 kB Inactive: 496968 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 451516 kB SwapTotal: 2097892 kB SwapFree: 2096728 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5612 kB Slab: 13944 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 19:02:37 (client local time) WITH STATUS 30 IN 952.576 SECONDS stats: 22107 0 952.576 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 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 (173 /sec) c decisions : 316278 (332 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 952.129 s c _______________________________________________________________________________ #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.88 0.94 0.97 2/54 4018 Raw data (stat): 4018 (runsolver) R 4017 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841146137 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0011 s] Raw data (loadavg): 0.90 0.94 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0017 s] Raw data (loadavg): 0.91 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0019 s] Raw data (loadavg): 0.93 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0025 s] Raw data (loadavg): 0.94 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0029 s] Raw data (loadavg): 0.95 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.003 s] Raw data (loadavg): 0.95 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0037 s] Raw data (loadavg): 0.96 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0033 s] Raw data (loadavg): 0.97 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0033 s] Raw data (loadavg): 0.97 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.004 s] Raw data (loadavg): 0.98 0.95 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.005 s] Raw data (loadavg): 0.98 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.98 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.005 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.005 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.006 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.005 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.005 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.006 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.006 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.007 s] Raw data (loadavg): 0.99 0.96 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.008 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.015 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.015 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4022 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/59 4026 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4075 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.03 s] Raw data (loadavg): 0.99 0.97 0.97 2/55 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+952.477 s] Raw data (loadavg): 0.99 0.97 0.97 1/53 4077 Raw data (stat): 4018 (minisat+_script) S 4017 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841146137 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 30 Real time (s): 952.477 CPU time (s): 952.576 CPU user time (s): 952.145 CPU system time (s): 0.430934 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1076796928 #### END VERIFIER DATA ####