Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc05.opb |
MD5SUM | 4f7891bf040f9fa135208e1a9808a8bc |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1430464 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 21 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 2097151 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 5242880 |
Number of bits of the biggest number in a constraint | 23 |
Biggest sum of numbers in a constraint | 81788220 |
Number of bits of the biggest sum of numbers | 27 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 6.00309 |
Number of variables | 1320 |
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 | 301 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-04-21 18:03:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16989 boxname=wulflinc20 idbench=1307 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4f7891bf040f9fa135208e1a9808a8bc /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-misc05.opb IDLAUNCH: 16989 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 685312 kB Buffers: 21744 kB Cached: 304616 kB SwapCached: 516 kB Active: 15504 kB Inactive: 312812 kB HighTotal: 131008 kB HighFree: 98812 kB LowTotal: 903652 kB LowFree: 586500 kB SwapTotal: 2097892 kB SwapFree: 2096480 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5116 kB Slab: 15468 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 18:20:20 (client local time) WITH STATUS 30 IN 1028.43 SECONDS stats: 16989 0 1028.43 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]---> Sorter-cost: 471 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 345]---> Adder-cost: 718 maxlim: 5243515 bits: 24/23 c ---[ 343]---> Sorter-cost: 4443 Base: 2 2 2 2 2 2 3 5 2 2 2 17 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: 371 maxlim: 235002 bits: 19/18 c ---[ 180]---> Adder-cost: 414 maxlim: 398330 bits: 20/19 c ---[ 178]---> Adder-cost: 414 maxlim: 418810 bits: 20/19 c ---[ 176]---> Adder-cost: 371 maxlim: 195835 bits: 19/18 c ---[ 174]---> Adder-cost: 414 maxlim: 400890 bits: 20/19 c ---[ 172]---> Adder-cost: 414 maxlim: 397050 bits: 20/19 c ---[ 170]---> Adder-cost: 414 maxlim: 416250 bits: 20/19 c ---[ 168]---> BDD-cost: 72 c ---[ 166]---> BDD-cost: 72 c ---[ 165]---> Sorter-cost: 1614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 1614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> BDD-cost: 98 c ---[ 134]---> BDD-cost: 20 c ---[ 133]---> BDD-cost: 20 c ---[ 132]---> BDD-cost: 20 c ---[ 131]---> BDD-cost: 20 c ---[ 130]---> BDD-cost: 20 c ---[ 129]---> BDD-cost: 20 c ---[ 128]---> BDD-cost: 23 c ---[ 127]---> BDD-cost: 23 c ---[ 126]---> BDD-cost: 23 c ---[ 125]---> BDD-cost: 23 c ---[ 124]---> BDD-cost: 23 c ---[ 123]---> BDD-cost: 23 c ---[ 122]---> BDD-cost: 23 c ---[ 121]---> BDD-cost: 23 c ---[ 120]---> BDD-cost: 23 c ---[ 119]---> BDD-cost: 23 c ---[ 118]---> BDD-cost: 23 c ---[ 117]---> BDD-cost: 23 c ---[ 115]---> BDD-cost: 22 c ---[ 114]---> BDD-cost: 22 c ---[ 113]---> BDD-cost: 22 c ---[ 112]---> BDD-cost: 22 c ---[ 111]---> BDD-cost: 22 c ---[ 110]---> BDD-cost: 22 c ---[ 109]---> BDD-cost: 22 c ---[ 108]---> BDD-cost: 22 c ---[ 107]---> BDD-cost: 22 c ---[ 106]---> BDD-cost: 22 c ---[ 105]---> BDD-cost: 22 c ---[ 104]---> BDD-cost: 24 c ---[ 103]---> BDD-cost: 24 c ---[ 102]---> BDD-cost: 24 c ---[ 101]---> BDD-cost: 24 c ---[ 100]---> BDD-cost: 24 c ---[ 99]---> BDD-cost: 24 c ---[ 98]---> BDD-cost: 19 c ---[ 97]---> BDD-cost: 19 c ---[ 96]---> BDD-cost: 19 c ---[ 95]---> BDD-cost: 19 c ---[ 94]---> BDD-cost: 19 c ---[ 93]---> BDD-cost: 19 c ---[ 92]---> BDD-cost: 23 c ---[ 91]---> BDD-cost: 23 c ---[ 90]---> BDD-cost: 23 c ---[ 89]---> BDD-cost: 23 c ---[ 88]---> BDD-cost: 23 c ---[ 87]---> BDD-cost: 23 c ---[ 86]---> BDD-cost: 23 c ---[ 85]---> BDD-cost: 23 c ---[ 84]---> BDD-cost: 23 c ---[ 83]---> BDD-cost: 23 c ---[ 82]---> BDD-cost: 23 c ---[ 81]---> BDD-cost: 23 c ---[ 80]---> BDD-cost: 23 c ---[ 79]---> BDD-cost: 23 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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 50230 151151 | 15068 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/12572 c -- var.elim.: 2000/12572 c -- var.elim.: 3000/12572 c -- var.elim.: 4000/12572 c -- var.elim.: 5000/12572 c -- var.elim.: 6000/12572 c -- var.elim.: 7000/12572 c -- var.elim.: 8000/12572 c -- var.elim.: 9000/12572 c -- var.elim.: 10000/12572 c -- var.elim.: 11000/12572 c -- var.elim.: 12000/12572 c -- var.elim.: 12572/12572 c -- var.elim.: 1000/5065 c -- var.elim.: 2000/5065 c -- var.elim.: 3000/5065 c -- var.elim.: 4000/5065 c -- var.elim.: 5000/5065 c -- var.elim.: 5065/5065 c -- var.elim.: 63/63 c -- var.elim.: 20/20 c -- var.elim.: 10/10 c -- var.elim.: 5/5 c -- subsuming c -- var.elim.: 857/857 c -- var.elim.: 746/746 c -- var.elim.: 540/540 c -- var.elim.: 203/203 c -- var.elim.: 7/7 c -- var.elim.: 5/5 c -- subsuming c -- var.elim.: 278/278 c -- var.elim.: 203/203 c -- var.elim.: 62/62 c -- subsuming c -- var.elim.: 124/124 c -- var.elim.: 33/33 c -- var.elim.: 11/11 c | 0 | 43932 145479 | -- 0 -- -- | -- | -4876/903 c | 0 | 43932 145479 | 17572 0 0 nan | 0.000 % | c | 100 | 43932 145479 | 19330 100 7553 75.5 | 11.641 % | c | 250 | 43918 145420 | 21256 248 21743 87.7 | 11.651 % | c | 475 | 43890 145302 | 23367 468 24692 52.8 | 11.673 % | c | 812 | 43890 145302 | 25703 805 38354 47.6 | 11.673 % | c | 1318 | 43890 145302 | 28274 1311 48923 37.3 | 11.673 % | c | 2077 | 43832 145101 | 31060 2066 73875 35.8 | 11.758 % | c ============================================================================== c (current CPU-time: 3.64744 s) c ============================================================================== c [1mFound solution: 1468288[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 13 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2264 | 43844 145133 | 13153 2253 79749 35.4 | 11.758 % | c -- subsuming c -- var.elim.: 100/100 c -- var.elim.: 67/67 c -- var.elim.: 23/23 c | 2264 | 43815 145084 | -- 2253 -- -- | -- | -29/-48 c | 2264 | 43815 145084 | 17526 2104 57169 27.2 | 11.758 % | c | 2364 | 43815 145084 | 19278 2204 59457 27.0 | 11.795 % | c | 2515 | 43769 144922 | 21184 2309 60197 26.1 | 11.870 % | c ============================================================================== c (current CPU-time: 4.24235 s) c ============================================================================== c [1mFound solution: 1460736[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 11 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2695 | 43765 144887 | 13129 2486 66466 26.7 | 11.870 % | c -- subsuming c -- var.elim.: 121/121 c -- var.elim.: 41/41 c -- var.elim.: 74/74 c -- var.elim.: 33/33 c | 2695 | 43687 144631 | -- 2486 -- -- | -- | -78/-255 c | 2695 | 43687 144631 | 17474 2486 66466 26.7 | 11.870 % | c ============================================================================== c (current CPU-time: 4.46232 s) c ============================================================================== c [1mFound solution: 1458688[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 10 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2710 | 43701 144663 | 13110 2501 69078 27.6 | 11.870 % | c -- subsuming c -- var.elim.: 27/27 c -- var.elim.: 12/12 c | 2710 | 43687 144627 | -- 2501 -- -- | -- | -14/-35 c | 2710 | 43687 144627 | 17474 2500 69076 27.6 | 11.870 % | c | 2810 | 43687 144627 | 19222 2600 78719 30.3 | 11.995 % | c | 2960 | 43687 144627 | 21144 2750 103424 37.6 | 11.995 % | c | 3185 | 42557 140921 | 22657 2959 107841 36.4 | 13.811 % | c ============================================================================== c (current CPU-time: 5.34019 s) c ============================================================================== c [1mFound solution: 1449600[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 13 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3202 | 42569 140952 | 12770 2976 108742 36.5 | 13.811 % | c -- subsuming c -- var.elim.: 569/569 c -- var.elim.: 269/269 c -- var.elim.: 10/10 c -- subsuming c -- var.elim.: 22/22 c -- var.elim.: 25/25 c | 3202 | 42478 140885 | -- 2976 -- -- | -- | -91/-66 c | 3202 | 42478 140885 | 16991 2848 84733 29.8 | 13.811 % | c | 3302 | 42417 140659 | 18663 2947 90603 30.7 | 13.983 % | c | 3452 | 42417 140659 | 20529 3097 95972 31.0 | 13.983 % | c | 3677 | 42417 140659 | 22582 3322 105822 31.9 | 13.983 % | c | 4014 | 42417 140659 | 24841 3659 149954 41.0 | 13.983 % | c | 4520 | 42300 140230 | 27249 4161 228626 54.9 | 14.145 % | c ============================================================================== c (current CPU-time: 8.41472 s) c ============================================================================== c [1mFound solution: 1434304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 14 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 4677 | 42297 140202 | 12689 4294 237298 55.3 | 14.145 % | c -- subsuming c -- var.elim.: 232/232 c -- var.elim.: 116/116 c -- var.elim.: 9/9 c -- subsuming c -- var.elim.: 38/38 c -- var.elim.: 12/12 c | 4677 | 42201 139962 | -- 4294 -- -- | -- | -96/-239 c | 4677 | 42201 139962 | 16880 4195 218272 52.0 | 14.145 % | c | 4777 | 42062 139500 | 18507 4293 222006 51.7 | 14.458 % | c | 4928 | 41632 138052 | 20149 4404 237169 53.9 | 15.158 % | c | 5154 | 41615 137990 | 22155 4628 246582 53.3 | 15.180 % | c | 5491 | 41582 137857 | 24352 4961 254950 51.4 | 15.212 % | c | 5998 | 41568 137798 | 26778 5467 270856 49.5 | 15.223 % | c | 6758 | 41568 137798 | 29456 6227 329443 52.9 | 15.223 % | c | 7897 | 41546 137713 | 32384 7357 386179 52.5 | 15.245 % | c | 9605 | 41509 137589 | 35591 9056 757717 83.7 | 15.320 % | c | 12167 | 41447 137359 | 39091 11609 1627586 140.2 | 15.395 % | c | 16014 | 41405 137182 | 42957 15444 2551827 165.2 | 15.428 % | c ============================================================================== c (current CPU-time: 48.6316 s) c ============================================================================== c [1mFound solution: 1430464[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> BDD-cost: 13 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 21241 | 41370 137014 | 12410 20658 4049133 196.0 | 15.428 % | c -- subsuming c -- var.elim.: 571/571 c -- var.elim.: 267/267 c -- var.elim.: 22/22 c -- subsuming c -- var.elim.: 18/18 c -- var.elim.: 13/13 c | 21241 | 41259 136829 | -- 20658 -- -- | -- | -111/-184 c | 21241 | 41259 136829 | 16503 13550 778514 57.5 | 15.428 % | c | 21341 | 41259 136829 | 18153 13650 787484 57.7 | 15.614 % | c | 21491 | 41259 136829 | 19969 13800 845944 61.3 | 15.614 % | c | 21716 | 41259 136829 | 21966 14025 924935 65.9 | 15.614 % | c | 22059 | 41259 136829 | 24162 14368 957833 66.7 | 15.614 % | c | 22566 | 41259 136829 | 26579 14875 1016471 68.3 | 15.614 % | c | 23326 | 41259 136829 | 29237 15635 1285597 82.2 | 15.614 % | c | 24466 | 41259 136829 | 32160 16775 1416124 84.4 | 15.614 % | c | 26174 | 41259 136829 | 35376 18483 1579792 85.5 | 15.614 % | c | 28737 | 41218 136646 | 38875 21002 1906828 90.8 | 15.657 % | c | 32581 | 41134 136333 | 42676 24839 4071089 163.9 | 15.755 % | c | 38348 | 41092 136168 | 46896 30596 6529756 213.4 | 15.809 % | c | 46998 | 40958 135626 | 51417 39176 10780063 275.2 | 15.950 % | c | 59973 | 40706 134771 | 56211 52131 19087926 366.2 | 16.318 % | c | 79434 | 40466 133868 | 61467 36593 16899698 461.8 | 16.643 % | c | 108626 | 40368 133483 | 67450 28321 10382829 366.6 | 16.784 % | c | 152415 | 40327 133320 | 74120 30951 9570614 309.2 | 16.827 % | c ============================================================================== c [1mOptimal solution: 1430464[0m s OPTIMUM FOUND v -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 -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_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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 c _______________________________________________________________________________ c c restarts : 49 c conflicts : 167096 (163 /sec) c decisions : 307193 (299 /sec) c propagations : 117032313 (113932 /sec) c inspects : 1230845345 (1198238 /sec) c CPU time : 1027.21 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.85 0.97 0.91 2/54 10458 Raw data (stat): 10458 (runsolver) R 10457 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547089163 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0001 s] Raw data (loadavg): 0.87 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 4621 0 0 0 984 14 0 0 25 0 1 0 547089163 13303808 2734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3248 2734 603 41 0 3207 0 vsize: 12992 [startup+20.0011 s] Raw data (loadavg): 0.89 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 5604 0 0 0 1982 16 0 0 25 0 1 0 547089163 17350656 3717 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4236 3717 603 41 0 4195 0 vsize: 16944 [startup+30.0018 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 6601 0 0 0 2979 19 0 0 25 0 1 0 547089163 21524480 4714 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5255 4714 603 41 0 5214 0 vsize: 21020 [startup+40.0014 s] Raw data (loadavg): 0.92 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 7720 0 0 0 3976 22 0 0 25 0 1 0 547089163 26132480 5833 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6380 5833 603 41 0 6339 0 vsize: 25520 [startup+50.0021 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8954 0 0 0 4971 26 0 0 25 0 1 0 547089163 30617600 6907 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7475 6907 603 41 0 7434 0 vsize: 29900 [startup+60.002 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8954 0 0 0 5970 26 0 0 25 0 1 0 547089163 30617600 6907 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7475 6907 603 41 0 7434 0 vsize: 29900 [startup+70.0024 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8957 0 0 0 6971 27 0 0 25 0 1 0 547089163 30617600 6910 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7475 6910 603 41 0 7434 0 vsize: 29900 [startup+80.0036 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 8959 0 0 0 7971 27 0 0 25 0 1 0 547089163 30617600 6912 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7475 6912 603 41 0 7434 0 vsize: 29900 [startup+90.0031 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 9773 0 0 0 8970 28 0 0 25 0 1 0 547089163 33816576 7726 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8256 7726 603 41 0 8215 0 vsize: 33024 [startup+100.004 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 10862 0 0 0 9966 32 0 0 25 0 1 0 547089163 38289408 8815 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9348 8815 603 41 0 9307 0 vsize: 37392 [startup+110.004 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 11806 0 0 0 10963 35 0 0 25 0 1 0 547089163 42172416 9759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10296 9759 603 41 0 10255 0 vsize: 41184 [startup+120.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 12542 0 0 0 11961 37 0 0 25 0 1 0 547089163 45223936 10495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11041 10495 603 41 0 11000 0 vsize: 44164 [startup+130.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 10458 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 13215 0 0 0 12959 39 0 0 25 0 1 0 547089163 48062464 11168 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11734 11168 603 41 0 11693 0 vsize: 46936 [startup+140.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 14308 0 0 0 13956 42 0 0 25 0 1 0 547089163 52563968 12261 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12833 12261 603 41 0 12792 0 vsize: 51332 [startup+150.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 15039 0 0 0 14955 44 0 0 25 0 1 0 547089163 55476224 12992 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13544 12992 603 41 0 13503 0 vsize: 54176 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 15888 0 0 0 15954 45 0 0 25 0 1 0 547089163 58974208 13841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14398 13841 603 41 0 14357 0 vsize: 57592 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 16621 0 0 0 16952 48 0 0 25 0 1 0 547089163 61968384 14574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15129 14574 603 41 0 15088 0 vsize: 60516 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 17538 0 0 0 17949 50 0 0 25 0 1 0 547089163 65740800 15491 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16050 15491 603 41 0 16009 0 vsize: 64200 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 18679 0 0 0 18947 52 0 0 25 0 1 0 547089163 70443008 16632 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17198 16632 603 41 0 17157 0 vsize: 68792 [startup+200.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 19607 0 0 0 19945 54 0 0 25 0 1 0 547089163 74129408 17560 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18098 17560 603 41 0 18057 0 vsize: 72392 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 20538 0 0 0 20943 57 0 0 25 0 1 0 547089163 77942784 18491 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19029 18491 603 41 0 18988 0 vsize: 76116 [startup+220.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 21444 0 0 0 21942 58 0 0 25 0 1 0 547089163 81711104 19397 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19949 19397 603 41 0 19908 0 vsize: 79796 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 22380 0 0 0 22940 60 0 0 25 0 1 0 547089163 85561344 20333 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20889 20333 603 41 0 20848 0 vsize: 83556 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 23200 0 0 0 23938 63 0 0 25 0 1 0 547089163 88850432 21153 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21692 21153 603 41 0 21651 0 vsize: 86768 [startup+250.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 23975 0 0 0 24936 65 0 0 25 0 1 0 547089163 92065792 21928 4294967295 134512640 134672761 3221224544 3221223688 134616279 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22477 21928 603 41 0 22436 0 vsize: 89908 [startup+260.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 24400 0 0 0 25935 65 0 0 25 0 1 0 547089163 93773824 22353 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22894 22353 603 41 0 22853 0 vsize: 91576 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 24836 0 0 0 26934 67 0 0 25 0 1 0 547089163 95555584 22789 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23329 22789 603 41 0 23288 0 vsize: 93316 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 25304 0 0 0 27933 68 0 0 25 0 1 0 547089163 97505280 23257 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23805 23257 603 41 0 23764 0 vsize: 95220 [startup+290.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 26237 0 0 0 28929 72 0 0 25 0 1 0 547089163 101277696 24190 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24726 24190 603 41 0 24685 0 vsize: 98904 [startup+300.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 26832 0 0 0 29928 74 0 0 25 0 1 0 547089163 103809024 24785 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25344 24785 603 41 0 25303 0 vsize: 101376 [startup+310.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 27731 0 0 0 30925 76 0 0 25 0 1 0 547089163 107487232 25684 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26242 25684 603 41 0 26201 0 vsize: 104968 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 31925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26204 603 41 0 26724 0 vsize: 107060 [startup+330.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 32925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26204 603 41 0 26724 0 vsize: 107060 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 33925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26204 603 41 0 26724 0 vsize: 107060 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 34925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26204 603 41 0 26724 0 vsize: 107060 [startup+360.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28310 0 0 0 35925 77 0 0 25 0 1 0 547089163 109629440 26204 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26204 603 41 0 26724 0 vsize: 107060 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28311 0 0 0 36926 77 0 0 25 0 1 0 547089163 109629440 26205 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26205 603 41 0 26724 0 vsize: 107060 [startup+380.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28311 0 0 0 37926 77 0 0 25 0 1 0 547089163 109629440 26205 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26205 603 41 0 26724 0 vsize: 107060 [startup+390.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28311 0 0 0 38926 77 0 0 25 0 1 0 547089163 109629440 26205 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26205 603 41 0 26724 0 vsize: 107060 [startup+400.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 39926 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26206 603 41 0 26724 0 vsize: 107060 [startup+410.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 40926 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26206 603 41 0 26724 0 vsize: 107060 [startup+420.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 41926 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26206 603 41 0 26724 0 vsize: 107060 [startup+430.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 42927 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26206 603 41 0 26724 0 vsize: 107060 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28312 0 0 0 43927 78 0 0 25 0 1 0 547089163 109629440 26206 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26206 603 41 0 26724 0 vsize: 107060 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28313 0 0 0 44927 78 0 0 25 0 1 0 547089163 109629440 26207 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26207 603 41 0 26724 0 vsize: 107060 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28313 0 0 0 45927 78 0 0 25 0 1 0 547089163 109629440 26207 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26207 603 41 0 26724 0 vsize: 107060 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28313 0 0 0 46927 78 0 0 25 0 1 0 547089163 109629440 26207 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26765 26207 603 41 0 26724 0 vsize: 107060 [startup+480.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 28940 0 0 0 47926 79 0 0 25 0 1 0 547089163 112279552 26834 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27412 26834 603 41 0 27371 0 vsize: 109648 [startup+490.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 29756 0 0 0 48923 82 0 0 25 0 1 0 547089163 115585024 27650 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28219 27650 603 41 0 28178 0 vsize: 112876 [startup+500.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 30785 0 0 0 49922 84 0 0 25 0 1 0 547089163 119943168 28679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29283 28679 603 41 0 29242 0 vsize: 117132 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 31521 0 0 0 50920 86 0 0 25 0 1 0 547089163 122839040 29415 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29990 29415 603 41 0 29949 0 vsize: 119960 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 32292 0 0 0 51918 88 0 0 25 0 1 0 547089163 126029824 30186 4294967295 134512640 134672761 3221224544 3221223584 134614268 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30769 30186 603 41 0 30728 0 vsize: 123076 [startup+530.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 33227 0 0 0 52915 91 0 0 25 0 1 0 547089163 129892352 31121 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31712 31121 603 41 0 31671 0 vsize: 126848 [startup+540.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 34032 0 0 0 53913 93 0 0 25 0 1 0 547089163 133185536 31926 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32516 31926 603 41 0 32475 0 vsize: 130064 [startup+550.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 34771 0 0 0 54912 94 0 0 25 0 1 0 547089163 136278016 32665 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33271 32665 603 41 0 33230 0 vsize: 133084 [startup+560.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 35414 0 0 0 55910 97 0 0 25 0 1 0 547089163 138870784 33308 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33904 33308 603 41 0 33863 0 vsize: 135616 [startup+570.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 35824 0 0 0 56909 98 0 0 25 0 1 0 547089163 140554240 33718 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34315 33718 603 41 0 34274 0 vsize: 137260 [startup+580.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 36622 0 0 0 57906 101 0 0 25 0 1 0 547089163 143839232 34516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35117 34516 603 41 0 35076 0 vsize: 140468 [startup+590.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 37049 0 0 0 58905 102 0 0 25 0 1 0 547089163 145637376 34943 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35556 34943 603 41 0 35515 0 vsize: 142224 [startup+600.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 37563 0 0 0 59904 104 0 0 25 0 1 0 547089163 147668992 35457 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36052 35457 603 41 0 36011 0 vsize: 144208 [startup+610.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 38158 0 0 0 60902 106 0 0 25 0 1 0 547089163 150061056 36052 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36636 36052 603 41 0 36595 0 vsize: 146544 [startup+620.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39031 0 0 0 61901 107 0 0 25 0 1 0 547089163 153718784 36925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37529 36925 603 41 0 37488 0 vsize: 150116 [startup+630.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39467 0 0 0 62899 109 0 0 25 0 1 0 547089163 155160576 37298 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37298 603 41 0 37840 0 vsize: 151524 [startup+640.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39467 0 0 0 63899 109 0 0 25 0 1 0 547089163 155160576 37298 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37298 603 41 0 37840 0 vsize: 151524 [startup+650.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39469 0 0 0 64900 109 0 0 25 0 1 0 547089163 155160576 37300 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37300 603 41 0 37840 0 vsize: 151524 [startup+660.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39469 0 0 0 65900 109 0 0 25 0 1 0 547089163 155160576 37300 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37300 603 41 0 37840 0 vsize: 151524 [startup+670.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39469 0 0 0 66900 109 0 0 25 0 1 0 547089163 155160576 37300 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37300 603 41 0 37840 0 vsize: 151524 [startup+680.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 67900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+690.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 68900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+700.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 69900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223356 1075350544 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+710.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 70900 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+720.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 71901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+730.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 72901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+740.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 73901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+750.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 74901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+760.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 75901 109 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+770.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 76901 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+780.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 77902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+790.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 78902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+800.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 79902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+810.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39470 0 0 0 80902 110 0 0 25 0 1 0 547089163 155160576 37301 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37301 603 41 0 37840 0 vsize: 151524 [startup+820.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39473 0 0 0 81902 110 0 0 25 0 1 0 547089163 155160576 37304 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37304 603 41 0 37840 0 vsize: 151524 [startup+830.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39473 0 0 0 82902 110 0 0 25 0 1 0 547089163 155160576 37304 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37304 603 41 0 37840 0 vsize: 151524 [startup+840.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39477 0 0 0 83903 110 0 0 25 0 1 0 547089163 155160576 37308 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37308 603 41 0 37840 0 vsize: 151524 [startup+850.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39478 0 0 0 84903 110 0 0 25 0 1 0 547089163 155160576 37309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37309 603 41 0 37840 0 vsize: 151524 [startup+860.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39478 0 0 0 85903 110 0 0 25 0 1 0 547089163 155160576 37309 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37309 603 41 0 37840 0 vsize: 151524 [startup+870.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39482 0 0 0 86903 110 0 0 25 0 1 0 547089163 155160576 37313 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37313 603 41 0 37840 0 vsize: 151524 [startup+880.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39482 0 0 0 87903 110 0 0 25 0 1 0 547089163 155160576 37313 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37881 37313 603 41 0 37840 0 vsize: 151524 [startup+890.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39484 0 0 0 88903 110 0 0 25 0 1 0 547089163 155422720 37315 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37945 37315 603 41 0 37904 0 vsize: 151780 [startup+900.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39485 0 0 0 89904 110 0 0 25 0 1 0 547089163 155422720 37316 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37945 37316 603 41 0 37904 0 vsize: 151780 [startup+910.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39486 0 0 0 90904 110 0 0 25 0 1 0 547089163 155422720 37317 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37945 37317 603 41 0 37904 0 vsize: 151780 [startup+920.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 39582 0 0 0 91904 110 0 0 25 0 1 0 547089163 155811840 37413 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38040 37413 603 41 0 37999 0 vsize: 152160 [startup+930.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40436 0 0 0 92901 113 0 0 25 0 1 0 547089163 159412224 38235 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38919 38235 603 41 0 38878 0 vsize: 155676 [startup+940.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 93902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+950.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 94902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+960.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 95902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+970.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 96902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+980.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 97902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+990.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 98902 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 99903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 100903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 101903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 155164 [startup+1028.28 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 10460 Raw data (stat): 10458 (minisat+) R 10457 27565 27564 0 -1 0 40440 0 0 0 101903 113 0 0 25 0 1 0 547089163 158887936 38170 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38791 38170 603 41 0 38750 0 vsize: 0 Child status: 30 Real time (s): 1028.28 CPU time (s): 1028.43 CPU user time (s): 1027.22 CPU system time (s): 1.20582 CPU usage (%): 100.014 Max. virtual memory (Kb): 155676 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 1430464 #### END VERIFIER DATA ####