Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-egout.opb |
MD5SUM | 46c4db5f8baf54496e00a723c85beb20 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 58880896 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1095 |
Biggest coefficient in the objective function | 533200896 |
Number of bits for the biggest coefficient in the objective function | 29 |
Sum of the numbers in the objective function | 14929722305 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 533200896 |
Number of bits of the biggest number in a constraint | 29 |
Biggest sum of numbers in a constraint | 14929722305 |
Number of bits of the biggest sum of numbers | 34 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.04084 |
Number of variables | 1155 |
Total number of constraints | 153 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 55 |
Number of constraints which are nor clauses,nor cardinality constraints | 98 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 280 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-04-21 05:39:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16795 boxname=wulflinc24 idbench=1292 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 46c4db5f8baf54496e00a723c85beb20 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-egout.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-egout.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 16795 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 631060 kB Buffers: 7672 kB Cached: 368956 kB SwapCached: 432 kB Active: 29596 kB Inactive: 349132 kB HighTotal: 131008 kB HighFree: 10192 kB LowTotal: 903652 kB LowFree: 620868 kB SwapTotal: 2097892 kB SwapFree: 2096708 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5932 kB Slab: 19180 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 05:59:28 (client local time) WITH STATUS 10 IN 1200.24 SECONDS stats: 16795 7 1200.24 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 115 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ########################### c -- Clauses(.)/Splits(s): (none) c ---[ 113]---> BDD-cost: 2069 c ---[ 111]---> BDD-cost: 40 c ---[ 109]---> BDD-cost: 25 c ---[ 107]---> BDD-cost: 45 c ---[ 105]---> BDD-cost: 83 c ---[ 101]---> BDD-cost: 39 c ---[ 99]---> BDD-cost: 100 c ---[ 97]---> BDD-cost: 34 c ---[ 91]---> BDD-cost: 55 c ---[ 89]---> BDD-cost: 40 c ---[ 85]---> BDD-cost: 128 c ---[ 83]---> BDD-cost: 40 c ---[ 81]---> BDD-cost: 112 c ---[ 79]---> BDD-cost: 49 c ---[ 75]---> BDD-cost: 45 c ---[ 73]---> BDD-cost: 28 c ---[ 71]---> BDD-cost: 214 c ---[ 69]---> BDD-cost: 55 c ---[ 67]---> BDD-cost: 123 c ---[ 65]---> BDD-cost: 118 c ---[ 59]---> BDD-cost: 51 c ---[ 57]---> BDD-cost: 40 c ---[ 55]---> BDD-cost: 40 c ---[ 53]---> BDD-cost: 51 c ---[ 49]---> BDD-cost: 135 c ---[ 47]---> BDD-cost: 135 c ---[ 45]---> BDD-cost: 49 c ---[ 44]---> BDD-cost: 9 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 9 c ---[ 41]---> BDD-cost: 10 c ---[ 40]---> BDD-cost: 10 c ---[ 39]---> BDD-cost: 11 c ---[ 37]---> BDD-cost: 12 c ---[ 36]---> BDD-cost: 12 c ---[ 35]---> BDD-cost: 12 c ---[ 34]---> BDD-cost: 12 c ---[ 31]---> BDD-cost: 12 c ---[ 30]---> BDD-cost: 12 c ---[ 29]---> BDD-cost: 13 c ---[ 27]---> BDD-cost: 26 c ---[ 26]---> BDD-cost: 26 c ---[ 25]---> BDD-cost: 26 c ---[ 24]---> BDD-cost: 26 c ---[ 23]---> BDD-cost: 26 c ---[ 21]---> BDD-cost: 10 c ---[ 20]---> BDD-cost: 10 c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 26 c ---[ 17]---> BDD-cost: 26 c ---[ 16]---> BDD-cost: 12 c ---[ 15]---> BDD-cost: 12 c ---[ 14]---> BDD-cost: 26 c ---[ 13]---> BDD-cost: 26 c ---[ 12]---> BDD-cost: 26 c ---[ 9]---> BDD-cost: 26 c ---[ 8]---> BDD-cost: 26 c ---[ 7]---> BDD-cost: 26 c ---[ 6]---> BDD-cost: 26 c ---[ 4]---> BDD-cost: 26 c ---[ 3]---> BDD-cost: 26 c ---[ 2]---> BDD-cost: 26 c ---[ 1]---> BDD-cost: 26 c ---[ 0]---> BDD-cost: 26 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11251 30877 | 3750 0 0 nan | 0.000 % | c | 100 | 11251 30877 | 4125 100 1515 15.2 | 13.712 % | c | 250 | 11125 30605 | 4537 201 3790 18.9 | 14.852 % | c ============================================================================== c [1mFound solution: 104597997[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:93787 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 312 | 275979 648913 | 91993 258 4502 17.4 | 14.852 % | c | 414 | 275839 648590 | 101192 359 5633 15.7 | 0.876 % | c | 566 | 273633 643567 | 111311 491 6737 13.7 | 1.527 % | c | 791 | 272629 641263 | 122442 694 11999 17.3 | 1.833 % | c | 1129 | 272332 640587 | 134686 1031 13927 13.5 | 1.923 % | c | 1637 | 269162 633419 | 148155 1521 18036 11.9 | 2.840 % | c | 2401 | 269146 633387 | 162971 2277 24619 10.8 | 2.849 % | c ============================================================================== c [1mFound solution: 103969862[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:62175 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2789 | 442636 1038731 | 147545 2648 27001 10.2 | 2.849 % | c | 2890 | 442630 1038719 | 162299 2746 28785 10.5 | 1.843 % | c | 3040 | 442133 1037580 | 178529 2873 30427 10.6 | 1.941 % | c | 3265 | 442133 1037580 | 196382 3098 33041 10.7 | 1.941 % | c | 3602 | 442099 1037510 | 216020 3421 35738 10.4 | 1.950 % | c ============================================================================== c [1mFound solution: 101568271[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3651 | 442571 1039056 | 147523 3469 36095 10.4 | 1.950 % | c | 3751 | 440803 1035063 | 162275 3568 36923 10.3 | 2.270 % | c | 3901 | 440803 1035063 | 178502 3718 37747 10.2 | 2.270 % | c | 4126 | 440579 1034544 | 196353 3940 39603 10.1 | 2.317 % | c | 4463 | 438220 1029144 | 215988 4267 46139 10.8 | 2.777 % | c ============================================================================== c [1mFound solution: 100803003[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:55983 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4817 | 593599 1391936 | 197866 4598 51840 11.3 | 2.777 % | c | 4917 | 593599 1391936 | 217652 4698 53220 11.3 | 2.178 % | c | 5068 | 593599 1391936 | 239417 4849 64015 13.2 | 2.178 % | c | 5294 | 593583 1391900 | 263359 5073 65615 12.9 | 2.180 % | c ============================================================================== c [1mFound solution: 100684650[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5609 | 594151 1393683 | 198050 5387 69571 12.9 | 2.180 % | c | 5709 | 594151 1393683 | 217855 5487 72393 13.2 | 2.178 % | c | 5859 | 593587 1392402 | 239640 5633 73644 13.1 | 2.255 % | c | 6084 | 592959 1390991 | 263604 5855 75225 12.8 | 2.341 % | c ============================================================================== c [1mFound solution: 92797205[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6220 | 593520 1392339 | 197840 5991 77445 12.9 | 2.341 % | c | 6320 | 593520 1392339 | 217624 6091 79073 13.0 | 2.338 % | c | 6470 | 591484 1387732 | 239386 6216 80899 13.0 | 2.618 % | c | 6696 | 591484 1387732 | 263325 6442 83338 12.9 | 2.618 % | c ============================================================================== c [1mFound solution: 83460735[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:45803 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6906 | 715900 1678230 | 238633 6632 89539 13.5 | 2.618 % | c | 7007 | 715884 1678194 | 262496 6732 92667 13.8 | 2.314 % | c | 7157 | 715884 1678194 | 288745 6882 105493 15.3 | 2.314 % | c | 7382 | 715685 1677751 | 317620 7102 134992 19.0 | 2.338 % | c | 7720 | 715422 1677166 | 349382 7431 137680 18.5 | 2.368 % | c | 8226 | 714699 1675530 | 384320 7925 140440 17.7 | 2.452 % | c ============================================================================== c [1mFound solution: 77397424[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8562 | 715491 1677827 | 238497 8258 144917 17.5 | 2.452 % | c | 8664 | 715379 1677582 | 262346 8356 145663 17.4 | 2.483 % | c | 8814 | 715364 1677550 | 288581 8505 146796 17.3 | 2.485 % | c | 9039 | 714976 1676674 | 317439 8719 151496 17.4 | 2.532 % | c | 9379 | 712783 1671706 | 349183 9013 167373 18.6 | 2.788 % | c | 9885 | 712783 1671706 | 384101 9519 195590 20.5 | 2.788 % | c ============================================================================== c [1mFound solution: 75180416[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:37038 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10054 | 811550 1902194 | 270516 9688 208790 21.6 | 2.788 % | c ============================================================================== c [1mFound solution: 73788603[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10119 | 812452 1904799 | 270817 9753 216393 22.2 | 2.788 % | c | 10219 | 811528 1902727 | 297898 9844 216942 22.0 | 2.723 % | c | 10369 | 810256 1899884 | 327688 9969 219537 22.0 | 2.845 % | c | 10594 | 810078 1899482 | 360457 10187 229042 22.5 | 2.862 % | c | 10934 | 809700 1898635 | 396503 10525 232743 22.1 | 2.897 % | c | 11440 | 809688 1898608 | 436153 11030 269210 24.4 | 2.899 % | c ============================================================================== c [1mFound solution: 70890816[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11567 | 808629 1896282 | 269543 11141 294797 26.5 | 2.899 % | c | 11667 | 808538 1896075 | 296497 11239 295298 26.3 | 3.045 % | c | 11820 | 808382 1895723 | 326147 11391 296270 26.0 | 3.061 % | c | 12045 | 808374 1895705 | 358761 11615 335819 28.9 | 3.062 % | c | 12383 | 807678 1894121 | 394637 11942 344697 28.9 | 3.132 % | c ============================================================================== c [1mFound solution: 70763968[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12669 | 807537 1893992 | 269179 12225 349850 28.6 | 3.132 % | c | 12769 | 807487 1893881 | 296096 12324 351330 28.5 | 3.154 % | c ============================================================================== c [1mFound solution: 70626176[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12794 | 807503 1893991 | 269167 12349 353606 28.6 | 3.154 % | c | 12896 | 807503 1893991 | 296083 12451 356275 28.6 | 3.154 % | c ============================================================================== c [1mFound solution: 70027776[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12938 | 807532 1894068 | 269177 12493 356758 28.6 | 3.154 % | c ============================================================================== c [1mFound solution: 70025856[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12974 | 807548 1894113 | 269182 12529 360715 28.8 | 3.154 % | c | 13075 | 807135 1893185 | 296100 12589 361725 28.7 | 3.201 % | c | 13225 | 807110 1893129 | 325710 12738 368507 28.9 | 3.204 % | c ============================================================================== c [1mFound solution: 68001664[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13371 | 807126 1893171 | 269042 12884 380444 29.5 | 3.204 % | c | 13471 | 807077 1893059 | 295946 12981 380994 29.4 | 3.209 % | c | 13621 | 807044 1892982 | 325540 13130 382392 29.1 | 3.214 % | c | 13846 | 807044 1892982 | 358094 13355 383733 28.7 | 3.214 % | c ============================================================================== c [1mFound solution: 65174016[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13997 | 807035 1892975 | 269011 13505 388162 28.7 | 3.214 % | c ============================================================================== c [1mFound solution: 62291456[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14037 | 807058 1893037 | 269019 13545 388559 28.7 | 3.214 % | c | 14137 | 807049 1893018 | 295920 13605 389920 28.7 | 3.222 % | c | 14287 | 807049 1893018 | 325512 13755 392019 28.5 | 3.222 % | c | 14512 | 807049 1893018 | 358064 13980 397143 28.4 | 3.222 % | c | 14851 | 807049 1893018 | 393870 14319 417509 29.2 | 3.222 % | c ============================================================================== c [1mFound solution: 62282321[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15069 | 807074 1893084 | 269024 14537 424496 29.2 | 3.222 % | c ============================================================================== c [1mFound solution: 62280682[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15106 | 807085 1893117 | 269028 14574 433145 29.7 | 3.222 % | c | 15207 | 807085 1893117 | 295930 14675 436853 29.8 | 3.223 % | c | 15358 | 807064 1893070 | 325523 14824 442215 29.8 | 3.225 % | c | 15583 | 807064 1893070 | 358076 15049 447226 29.7 | 3.225 % | c | 15920 | 807064 1893070 | 393883 15386 453459 29.5 | 3.225 % | c | 16426 | 807064 1893070 | 433272 15892 469778 29.6 | 3.225 % | c ============================================================================== c [1mFound solution: 62227456[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16835 | 807075 1893101 | 269025 16301 485940 29.8 | 3.225 % | c | 16939 | 807075 1893101 | 295927 16405 488704 29.8 | 3.226 % | c | 17089 | 807075 1893101 | 325520 16555 492833 29.8 | 3.226 % | c | 17314 | 807075 1893101 | 358072 16780 500117 29.8 | 3.226 % | c | 17651 | 807075 1893101 | 393879 17117 513203 30.0 | 3.226 % | c | 18157 | 807075 1893101 | 433267 17623 525729 29.8 | 3.226 % | c | 18916 | 806798 1892471 | 476594 17898 539622 30.1 | 3.261 % | c ============================================================================== c [1mFound solution: 62187392[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19541 | 806810 1892502 | 268936 18523 588761 31.8 | 3.261 % | c | 19642 | 806810 1892502 | 295829 18624 596304 32.0 | 3.261 % | c | 19792 | 806810 1892502 | 325412 18774 601693 32.0 | 3.261 % | c ============================================================================== c [1mFound solution: 62183922[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19829 | 806828 1892551 | 268942 18811 603364 32.1 | 3.261 % | c ============================================================================== c [1mFound solution: 62094660[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19849 | 806849 1892602 | 268949 18831 605524 32.2 | 3.261 % | c ============================================================================== c [1mFound solution: 62092608[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19920 | 806861 1892632 | 268953 18902 607820 32.2 | 3.261 % | c ============================================================================== c [1mFound solution: 62091582[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19938 | 806885 1892690 | 268961 18920 609878 32.2 | 3.261 % | c ============================================================================== c [1mFound solution: 62076192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19949 | 806903 1892732 | 268967 18931 611632 32.3 | 3.261 % | c ============================================================================== c [1mFound solution: 62063880[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19953 | 806917 1892772 | 268972 18935 611739 32.3 | 3.261 % | c ============================================================================== c [1mFound solution: 62060802[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19955 | 806934 1892819 | 268978 18937 612184 32.3 | 3.261 % | c ============================================================================== c [1mFound solution: 62048640[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19964 | 806947 1892853 | 268982 18946 613024 32.4 | 3.261 % | c ============================================================================== c [1mFound solution: 61994112[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19984 | 806963 1892892 | 268987 18966 613589 32.4 | 3.261 % | c | 20085 | 806963 1892892 | 295885 19067 618175 32.4 | 3.263 % | c | 20239 | 806963 1892892 | 325474 19221 629026 32.7 | 3.263 % | c | 20464 | 806963 1892892 | 358021 19446 637755 32.8 | 3.263 % | c | 20801 | 806963 1892892 | 393823 19783 655589 33.1 | 3.263 % | c | 21308 | 806963 1892892 | 433206 20290 688527 33.9 | 3.263 % | c | 22067 | 806963 1892892 | 476526 21049 718717 34.1 | 3.263 % | c ============================================================================== c [1mFound solution: 61947942[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22419 | 806856 1892653 | 268952 21400 735156 34.4 | 3.263 % | c | 22519 | 806856 1892653 | 295847 21500 736809 34.3 | 3.275 % | c ============================================================================== c [1mFound solution: 61892736[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22581 | 806871 1892688 | 268957 21562 739420 34.3 | 3.275 % | c ============================================================================== c [1mFound solution: 61163008[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22624 | 806889 1892730 | 268963 21605 745725 34.5 | 3.275 % | c | 22725 | 806889 1892730 | 295859 21706 752916 34.7 | 3.276 % | c | 22877 | 806889 1892730 | 325445 21858 760442 34.8 | 3.276 % | c | 23102 | 806889 1892730 | 357989 22083 767078 34.7 | 3.276 % | c | 23439 | 806889 1892730 | 393788 22420 780500 34.8 | 3.276 % | c | 23950 | 806889 1892730 | 433167 22931 812292 35.4 | 3.276 % | c | 24709 | 806889 1892730 | 476484 23690 835996 35.3 | 3.276 % | c | 25848 | 806889 1892730 | 524132 24829 896161 36.1 | 3.276 % | c ============================================================================== c [1mFound solution: 61074176[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26578 | 806893 1892748 | 268964 25558 923539 36.1 | 3.276 % | c | 26681 | 806893 1892748 | 295860 25661 929030 36.2 | 3.278 % | c | 26833 | 806893 1892748 | 325446 25813 934761 36.2 | 3.278 % | c | 27059 | 806893 1892748 | 357991 26039 948932 36.4 | 3.278 % | c | 27397 | 806893 1892748 | 393790 26377 962574 36.5 | 3.278 % | c | 27903 | 806893 1892748 | 433169 26883 982580 36.6 | 3.278 % | c | 28662 | 806893 1892748 | 476486 27642 1038039 37.6 | 3.278 % | c | 29803 | 806893 1892748 | 524134 28783 1085148 37.7 | 3.278 % | c | 31511 | 806893 1892748 | 576548 30491 1158917 38.0 | 3.278 % | c c *** TERMINATED *** s SATISFIABLE v I_0x2e_001_0x2e__0x2e__0x2e__bit0 -I_0x2e_001003_bit0 -I_0x2e_002003_bit0 -I_0x2e_002_0x2e__0x2e__0x2e__bit0 -I_0x2e_003005_bit0 I_0x2e_004005_bit0 -I_0x2e_004_0x2e__0x2e__0x2e__bit0 I_0x2e_005007_bit0 I_0x2e_006007_bit0 I_0x2e_007008_bit0 -I_0x2e_008_0x2e__0x2e__0x2e__bit0 I_0x2e_008009_bit0 I_0x2e_010012_bit0 I_0x2e_011012_bit0 -I_0x2e_012_0x2e__0x2e__0x2e__bit0 I_0x2e_012013_bit0 I_0x2e_013016_bit0 -I_0x2e_014015_bit0 I_0x2e_015016_bit0 -I_0x2e_016_0x2e__0x2e__0x2e__bit0 I_0x2e_016017_bit0 I_0x2e_017018_bit0 I_0x2e_009018_bit0 I_0x2e_018019_bit0 I_0x2e_019024_bit0 I_0x2e_024_0x2e__0x2e__0x2e__bit0 -I_0x2e_023024_bit0 -I_0x2e_022023_bit0 -I_0x2e_020022_bit0 I_0x2e_021022_bit0 I_0x2e_022_0x2e__0x2e__0x2e__bit0 -I_0x2e_024026_bit0 I_0x2e_025026_bit0 -I_0x2e_025_0x2e__0x2e__0x2e__bit0 I_0x2e_026027_bit0 I_0x2e_027_0x2e__0x2e__0x2e__bit0 -I_0x2e_027032_bit0 -I_0x2e_030031_bit0 I_0x2e_031032_bit0 I_0x2e_029031_bit0 -I_0x2e_028029_bit0 -I_0x2e_028_0x2e__0x2e__0x2e__bit0 I_0x2e_032033_bit0 I_0x2e_033037_bit0 -I_0x2e_036037_bit0 -I_0x2e_034036_bit0 -I_0x2e_035036_bit0 I_0x2e_037038_bit0 I_0x2e_038040_bit0 I_0x2e_039040_bit0 -I_0x2e_040_0x2e__0x2e__0x2e__bit0 -I_0x2e_041_0x2e__0x2e__0x2e__bit0 I_0x2e_040041_bit0 I_0x2e_041042_bit0 I_0x2e_042_0x2e__0x2e__0x2e__bit0 -F_0x2e_001_0x2e__0x2e__0x2e__bit_7 -F_0x2e_001_0x2e__0x2e__0x2e__bit_6 -F_0x2e_001_0x2e__0x2e__0x2e__bit_5 -F_0x2e_001_0x2e__0x2e__0x2e__bit_4 -F_0x2e_001_0x2e__0x2e__0x2e__bit_3 -F_0x2e_001_0x2e__0x2e__0x2e__bit_2 -F_0x2e_001_0x2e__0x2e__0x2e__bit_1 -F_0x2e_001_0x2e__0x2e__0x2e__bit0 F_0x2e_001_0x2e__0x2e__0x2e__bit1 -F_0x2e_001_0x2e__0x2e__0x2e__bit2 -F_0x2e_001_0x2e__0x2e__0x2e__bit3 -F_0x2e_001_0x2e__0x2e__0x2e__bit4 -F_0x2e_001_0x2e__0x2e__0x2e__bit5 -F_0x2e_001_0x2e__0x2e__0x2e__bit6 -F_0x2e_001_0x2e__0x2e__0x2e__bit7 -F_0x2e_001_0x2e__0x2e__0x2e__bit8 -F_0x2e_001_0x2e__0x2e__0x2e__bit9 -F_0x2e_001_0x2e__0x2e__0x2e__bit10 -F_0x2e_001_0x2e__0x2e__0x2e__bit11 -F_0x2e_001_0x2e__0x2e__0x2e__bit12 -F_0x2e_001003_bit_7 -F_0x2e_001003_bit_6 -F_0x2e_001003_bit_5 -F_0x2e_001003_bit_4 -F_0x2e_001003_bit_3 -F_0x2e_001003_bit_2 -F_0x2e_001003_bit_1 -F_0x2e_001003_bit0 -F_0x2e_001003_bit1 -F_0x2e_001003_bit2 -F_0x2e_001003_bit3 -F_0x2e_001003_bit4 -F_0x2e_001003_bit5 -F_0x2e_001003_bit6 -F_0x2e_001003_bit7 -F_0x2e_001003_bit8 -F_0x2e_001003_bit9 -F_0x2e_001003_bit10 -F_0x2e_001003_bit11 -F_0x2e_001003_bit12 -F_0x2e_002003_bit_7 -F_0x2e_002003_bit_6 -F_0x2e_002003_bit_5 -F_0x2e_002003_bit_4 -F_0x2e_002003_bit_3 -F_0x2e_002003_bit_2 -F_0x2e_002003_bit_1 -F_0x2e_002003_bit0 -F_0x2e_002003_bit1 -F_0x2e_002003_bit2 -F_0x2e_002003_bit3 -F_0x2e_002003_bit4 -F_0x2e_002003_bit5 -F_0x2e_002003_bit6 -F_0x2e_002003_bit7 -F_0x2e_002003_bit8 -F_0x2e_002003_bit9 -F_0x2e_002003_bit10 -F_0x2e_002003_bit11 -F_0x2e_002003_bit12 -F_0x2e_002_0x2e__0x2e__0x2e__bit_7 -F_0x2e_002_0x2e__0x2e__0x2e__bit_6 -F_0x2e_002_0x2e__0x2e__0x2e__bit_5 -F_0x2e_002_0x2e__0x2e__0x2e__bit_4 -F_0x2e_002_0x2e__0x2e__0x2e__bit_3 -F_0x2e_002_0x2e__0x2e__0x2e__bit_2 -F_0x2e_002_0x2e__0x2e__0x2e__bit_1 -F_0x2e_002_0x2e__0x2e__0x2e__bit0 -F_0x2e_002_0x2e__0x2e__0x2e__bit1 -F_0x2e_002_0x2e__0x2e__0x2e__bit2 -F_0x2e_002_0x2e__0x2e__0x2e__bit3 -F_0x2e_002_0x2e__0x2e__0x2e__bit4 -F_0x2e_002_0x2e__0x2e__0x2e__bit5 -F_0x2e_002_0x2e__0x2e__0x2e__bit6 -F_0x2e_002_0x2e__0x2e__0x2e__bit7 -F_0x2e_002_0x2e__0x2e__0x2e__bit8 -F_0x2e_002_0x2e__0x2e__0x2e__bit9 -F_0x2e_002_0x2e__0x2e__0x2e__bit10 -F_0x2e_002_0x2e__0x2e__0x2e__bit11 -F_0x2e_002_0x2e__0x2e__0x2e__bit12 -F_0x2e_003005_bit_7 -F_0x2e_003005_bit_6 -F_0x2e_003005_bit_5 -F_0x2e_003005_bit_4 -F_0x2e_003005_bit_3 -F_0x2e_003005_bit_2 -F_0x2e_003005_bit_1 -F_0x2e_003005_bit0 -F_0x2e_003005_bit1 -F_0x2e_003005_bit2 -F_0x2e_003005_bit3 -F_0x2e_003005_bit4 -F_0x2e_003005_bit5 -F_0x2e_003005_bit6 -F_0x2e_003005_bit7 -F_0x2e_003005_bit8 -F_0x2e_003005_bit9 -F_0x2e_003005_bit10 -F_0x2e_003005_bit11 -F_0x2e_003005_bit12 -F_0x2e_004005_bit_7 -F_0x2e_004005_bit_6 -F_0x2e_004005_bit_5 -F_0x2e_004005_bit_4 -F_0x2e_004005_bit_3 -F_0x2e_004005_bit_2 -F_0x2e_004005_bit_1 F_0x2e_004005_bit0 F_0x2e_004005_bit1 F_0x2e_004005_bit2 -F_0x2e_004005_bit3 -F_0x2e_004005_bit4 -F_0x2e_004005_bit5 -F_0x2e_004005_bit6 -F_0x2e_004005_bit7 -F_0x2e_004005_bit8 -F_0x2e_004005_bit9 -F_0x2e_004005_bit10 -F_0x2e_004005_bit11 -F_0x2e_004005_bit12 -F_0x2e_004_0x2e__0x2e__0x2e__bit_7 -F_0x2e_004_0x2e__0x2e__0x2e__bit_6 -F_0x2e_004_0x2e__0x2e__0x2e__bit_5 -F_0x2e_004_0x2e__0x2e__0x2e__bit_4 -F_0x2e_004_0x2e__0x2e__0x2e__bit_3 -F_0x2e_004_0x2e__0x2e__0x2e__bit_2 -F_0x2e_004_0x2e__0x2e__0x2e__bit_1 -F_0x2e_004_0x2e__0x2e__0x2e__bit0 -F_0x2e_004_0x2e__0x2e__0x2e__bit1 -F_0x2e_004_0x2e__0x2e__0x2e__bit2 -F_0x2e_004_0x2e__0x2e__0x2e__bit3 -F_0x2e_004_0x2e__0x2e__0x2e__bit4 -F_0x2e_004_0x2e__0x2e__0x2e__bit5 -F_0x2e_004_0x2e__0x2e__0x2e__bit6 -F_0x2e_004_0x2e__0x2e__0x2e__bit7 -F_0x2e_004_0x2e__0x2e__0x2e__bit8 -F_0x2e_004_0x2e__0x2e__0x2e__bit9 -F_0x2e_004_0x2e__0x2e__0x2e__bit10 -F_0x2e_004_0x2e__0x2e__0x2e__bit11 -F_0x2e_004_0x2e__0x2e__0x2e__bit12 -F_0x2e_005007_bit_7 -F_0x2e_005007_bit_6 -F_0x2e_005007_bit_5 -F_0x2e_005007_bit_4 -F_0x2e_005007_bit_3 -F_0x2e_005007_bit_2 -F_0x2e_005007_bit_1 F_0x2e_005007_bit0 F_0x2e_005007_bit1 F_0x2e_005007_bit2 -F_0x2e_005007_bit3 -F_0x2e_005007_bit4 -F_0x2e_005007_bit5 -F_0x2e_005007_bit6 -F_0x2e_005007_bit7 -F_0x2e_005007_bit8 -F_0x2e_005007_bit9 -F_0x2e_005007_bit10 -F_0x2e_005007_bit11 -F_0x2e_005007_bit12 -F_0x2e_006007_bit_7 -F_0x2e_006007_bit_6 -F_0x2e_006007_bit_5 -F_0x2e_006007_bit_4 -F_0x2e_006007_bit_3 -F_0x2e_006007_bit_2 -F_0x2e_006007_bit_1 -F_0x2e_006007_bit0 -F_0x2e_006007_bit1 F_0x2e_006007_bit2 -F_0x2e_006007_bit3 -F_0x2e_006007_bit4 -F_0x2e_006007_bit5 -F_0x2e_006007_bit6 -F_0x2e_006007_bit7 -F_0x2e_006007_bit8 -F_0x2e_006007_bit9 -F_0x2e_006007_bit10 -F_0x2e_006007_bit11 -F_0x2e_006007_bit12 -F_0x2e_007008_bit_7 -F_0x2e_007008_bit_6 -F_0x2e_007008_bit_5 -F_0x2e_007008_bit_4 -F_0x2e_007008_bit_3 -F_0x2e_007008_bit_2 -F_0x2e_007008_bit_1 -F_0x2e_007008_bit0 -F_0x2e_007008_bit1 F_0x2e_007008_bit2 F_0x2e_007008_bit3 -F_0x2e_007008_bit4 -F_0x2e_007008_bit5 -F_0x2e_007008_bit6 -F_0x2e_007008_bit7 -F_0x2e_007008_bit8 -F_0x2e_007008_bit9 -F_0x2e_007008_bit10 -F_0x2e_007008_bit11 -F_0x2e_007008_bit12 -F_0x2e_008_0x2e__0x2e__0x2e__bit_7 -F_0x2e_008_0x2e__0x2e__0x2e__bit_6 -F_0x2e_008_0x2e__0x2e__0x2e__bit_5 -F_0x2e_008_0x2e__0x2e__0x2e__bit_4 -F_0x2e_008_0x2e__0x2e__0x2e__bit_3 -F_0x2e_008_0x2e__0x2e__0x2e__bit_2 -F_0x2e_008_0x2e__0x2e__0x2e__bit_1 -F_0x2e_008_0x2e__0x2e__0x2e__bit0 -F_0x2e_008_0x2e__0x2e__0x2e__bit1 -F_0x2e_008_0x2e__0x2e__0x2e__bit2 -F_0x2e_008_0x2e__0x2e__0x2e__bit3 -F_0x2e_008_0x2e__0x2e__0x2e__bit4 -F_0x2e_008_0x2e__0x2e__0x2e__bit5 -F_0x2e_008_0x2e__0x2e__0x2e__bit6 -F_0x2e_008_0x2e__0x2e__0x2e__bit7 -F_0x2e_008_0x2e__0x2e__0x2e__bit8 -F_0x2e_008_0x2e__0x2e__0x2e__bit9 -F_0x2e_008_0x2e__0x2e__0x2e__bit10 -F_0x2e_008_0x2e__0x2e__0x2e__bit11 -F_0x2e_008_0x2e__0x2e__0x2e__bit12 -F_0x2e_008009_bit_7 -F_0x2e_008009_bit_6 -F_0x2e_008009_bit_5 -F_0x2e_008009_bit_4 -F_0x2e_008009_bit_3 -F_0x2e_008009_bit_2 -F_0x2e_008009_bit_1 -F_0x2e_008009_bit0 -F_0x2e_008009_bit1 F_0x2e_008009_bit2 F_0x2e_008009_bit3 -F_0x2e_008009_bit4 -F_0x2e_008009_bit5 -F_0x2e_008009_bit6 -F_0x2e_008009_bit7 -F_0x2e_008009_bit8 -F_0x2e_008009_bit9 -F_0x2e_008009_bit10 -F_0x2e_008009_bit11 -F_0x2e_008009_bit12 -F_0x2e_010012_bit_7 -F_0x2e_010012_bit_6 -F_0x2e_010012_bit_5 -F_0x2e_010012_bit_4 -F_0x2e_010012_bit_3 -F_0x2e_010012_bit_2 -F_0x2e_010012_bit_1 F_0x2e_010012_bit0 -F_0x2e_010012_bit1 -F_0x2e_010012_bit2 -F_0x2e_010012_bit3 -F_0x2e_010012_bit4 -F_0x2e_010012_bit5 -F_0x2e_010012_bit6 -F_0x2e_010012_bit7 -F_0x2e_010012_bit8 -F_0x2e_010012_bit9 -F_0x2e_010012_bit10 -F_0x2e_010012_bit11 -F_0x2e_010012_bit12 -F_0x2e_012_0x2e__0x2e__0x2e__bit_7 -F_0x2e_012_0x2e__0x2e__0x2e__bit_6 -F_0x2e_012_0x2e__0x2e__0x2e__bit_5 -F_0x2e_012_0x2e__0x2e__0x2e__bit_4 -F_0x2e_012_0x2e__0x2e__0x2e__bit_3 -F_0x2e_012_0x2e__0x2e__0x2e__bit_2 -F_0x2e_012_0x2e__0x2e__0x2e__bit_1 -F_0x2e_012_0x2e__0x2e__0x2e__bit0 -F_0x2e_012_0x2e__0x2e__0x2e__bit1 -F_0x2e_012_0x2e__0x2e__0x2e__bit2 -F_0x2e_012_0x2e__0x2e__0x2e__bit3 -F_0x2e_012_0x2e__0x2e__0x2e__bit4 -F_0x2e_012_0x2e__0x2e__0x2e__bit5 -F_0x2e_012_0x2e__0x2e__0x2e__bit6 -F_0x2e_012_0x2e__0x2e__0x2e__bit7 -F_0x2e_012_0x2e__0x2e__0x2e__bit8 -F_0x2e_012_0x2e__0x2e__0x2e__bit9 -F_0x2e_012_0x2e__0x2e__0x2e__bit10 -F_0x2e_012_0x2e__0x2e__0x2e__bit11 -F_0x2e_012_0x2e__0x2e__0x2e__bit12 -F_0x2e_012013_bit_7 -F_0x2e_012013_bit_6 -F_0x2e_012013_bit_5 -F_0x2e_012013_bit_4 -F_0x2e_012013_bit_3 -F_0x2e_012013_bit_2 -F_0x2e_012013_bit_1 -F_0x2e_012013_bit0 F_0x2e_012013_bit1 F_0x2e_012013_bit2 -F_0x2e_012013_bit3 F_0x2e_012013_bit4 -F_0x2e_012013_bit5 -F_0x2e_012013_bit6 -F_0x2e_012013_bit7 -F_0x2e_012013_bit8 -F_0x2e_012013_bit9 -F_0x2e_012013_bit10 -F_0x2e_012013_bit11 -F_0x2e_012013_bit12 -F_0x2e_013016_bit_7 -F_0x2e_013016_bit_6 -F_0x2e_013016_bit_5 -F_0x2e_013016_bit_4 -F_0x2e_013016_bit_3 -F_0x2e_013016_bit_2 -F_0x2e_013016_bit_1 -F_0x2e_013016_bit0 F_0x2e_013016_bit1 -F_0x2e_013016_bit2 F_0x2e_013016_bit3 F_0x2e_013016_bit4 -F_0x2e_013016_bit5 -F_0x2e_013016_bit6 -F_0x2e_013016_bit7 -F_0x2e_013016_bit8 -F_0x2e_013016_bit9 -F_0x2e_013016_bit10 -F_0x2e_013016_bit11 -F_0x2e_013016_bit12 -F_0x2e_014015_bit_7 -F_0x2e_014015_bit_6 -F_0x2e_014015_bit_5 -F_0x2e_014015_bit_4 -F_0x2e_014015_bit_3 -F_0x2e_014015_bit_2 -F_0x2e_014015_bit_1 -F_0x2e_014015_bit0 -F_0x2e_014015_bit1 -F_0x2e_014015_bit2 -F_0x2e_014015_bit3 -F_0x2e_014015_bit4 -F_0x2e_014015_bit5 -F_0x2e_014015_bit6 -F_0x2e_014015_bit7 -F_0x2e_014015_bit8 -F_0x2e_014015_bit9 -F_0x2e_014015_bit10 -F_0x2e_014015_bit11 -F_0x2e_014015_bit12 -F_0x2e_015016_bit_7 -F_0x2e_015016_bit_6 -F_0x2e_015016_bit_5 -F_0x2e_015016_bit_4 -F_0x2e_015016_bit_3 -F_0x2e_015016_bit_2 -F_0x2e_015016_bit_1 F_0x2e_015016_bit0 -F_0x2e_015016_bit1 -F_0x2e_015016_bit2 -F_0x2e_015016_bit3 -F_0x2e_015016_bit4 -F_0x2e_015016_bit5 -F_0x2e_015016_bit6 -F_0x2e_015016_bit7 -F_0x2e_015016_bit8 -F_0x2e_015016_bit9 -F_0x2e_015016_bit10 -F_0x2e_015016_bit11 -F_0x2e_015016_bit12 -F_0x2e_016_0x2e__0x2e__0x2e__bit_7 -F_0x2e_016_0x2e__0x2e__0x2e__bit_6 -F_0x2e_016_0x2e__0x2e__0x2e__bit_5 -F_0x2e_016_0x2e__0x2e__0x2e__bit_4 -F_0x2e_016_0x2e__0x2e__0x2e__bit_3 -F_0x2e_016_0x2e__0x2e__0x2e__bit_2 -F_0x2e_016_0x2e__0x2e__0x2e__bit_1 -F_0x2e_016_0x2e__0x2e__0x2e__bit0 -F_0x2e_016_0x2e__0x2e__0x2e__bit1 -F_0x2e_016_0x2e__0x2e__0x2e__bit2 -F_0x2e_016_0x2e__0x2e__0x2e__bit3 -F_0x2e_016_0x2e__0x2e__0x2e__bit4 -F_0x2e_016_0x2e__0x2e__0x2e__bit5 -F_0x2e_016_0x2e__0x2e__0x2e__bit6 -F_0x2e_016_0x2e__0x2e__0x2e__bit7 -F_0x2e_016_0x2e__0x2e__0x2e__bit8 -F_0x2e_016_0x2e__0x2e__0x2e__bit9 -F_0x2e_016_0x2e__0x2e__0x2e__bit10 -F_0x2e_016_0x2e__0x2e__0x2e__bit11 -F_0x2e_016_0x2e__0x2e__0x2e__bit12 -F_0x2e_016017_bit_7 -F_0x2e_016017_bit_6 -F_0x2e_016017_bit_5 -F_0x2e_016017_bit_4 -F_0x2e_016017_bit_3 -F_0x2e_016017_bit_2 -F_0x2e_016017_bit_1 F_0x2e_016017_bit0 F_0x2e_016017_bit1 -F_0x2e_016017_bit2 F_0x2e_016017_bit3 F_0x2e_016017_bit4 -F_0x2e_016017_bit5 -F_0x2e_016017_bit6 -F_0x2e_016017_bit7 -F_0x2e_016017_bit8 -F_0x2e_016017_bit9 -F_0x2e_016017_bit10 -F_0x2e_016017_bit11 -F_0x2e_016017_bit12 -F_0x2e_017018_bit_7 -F_0x2e_017018_bit_6 -F_0x2e_017018_bit_5 -F_0x2e_017018_bit_4 -F_0x2e_017018_bit_3 -F_0x2e_017018_bit_2 -F_0x2e_017018_bit_1 F_0x2e_017018_bit0 F_0x2e_017018_bit1 -F_0x2e_017018_bit2 F_0x2e_017018_bit3 F_0x2e_017018_bit4 -F_0x2e_017018_bit5 -F_0x2e_017018_bit6 -F_0x2e_017018_bit7 -F_0x2e_017018_bit8 -F_0x2e_017018_bit9 -F_0x2e_017018_bit10 -F_0x2e_017018_bit11 -F_0x2e_017018_bit12 -F_0x2e_009018_bit_7 -F_0x2e_009018_bit_6 -F_0x2e_009018_bit_5 -F_0x2e_009018_bit_4 -F_0x2e_009018_bit_3 -F_0x2e_009018_bit_2 -F_0x2e_009018_bit_1 -F_0x2e_009018_bit0 -F_0x2e_009018_bit1 F_0x2e_009018_bit2 F_0x2e_009018_bit3 -F_0x2e_009018_bit4 -F_0x2e_009018_bit5 -F_0x2e_009018_bit6 -F_0x2e_009018_bit7 -F_0x2e_009018_bit8 -F_0x2e_009018_bit9 -F_0x2e_009018_bit10 -F_0x2e_009018_bit11 -F_0x2e_009018_bit12 -F_0x2e_018019_bit_7 -F_0x2e_018019_bit_6 -F_0x2e_018019_bit_5 -F_0x2e_018019_bit_4 -F_0x2e_018019_bit_3 -F_0x2e_018019_bit_2 -F_0x2e_018019_bit_1 F_0x2e_018019_bit0 F_0x2e_018019_bit1 F_0x2e_018019_bit2 -F_0x2e_018019_bit3 -F_0x2e_018019_bit4 F_0x2e_018019_bit5 -F_0x2e_018019_bit6 -F_0x2e_018019_bit7 -F_0x2e_018019_bit8 -F_0x2e_018019_bit9 -F_0x2e_018019_bit10 -F_0x2e_018019_bit11 -F_0x2e_018019_bit12 -F_0x2e_019024_bit_7 -F_0x2e_019024_bit_6 -F_0x2e_019024_bit_5 -F_0x2e_019024_bit_4 -F_0x2e_019024_bit_3 -F_0x2e_019024_bit_2 -F_0x2e_019024_bit_1 F_0x2e_019024_bit0 -F_0x2e_019024_bit1 -F_0x2e_019024_bit2 F_0x2e_019024_bit3 -F_0x2e_019024_bit4 F_0x2e_019024_bit5 -F_0x2e_019024_bit6 -F_0x2e_019024_bit7 -F_0x2e_019024_bit8 -F_0x2e_019024_bit9 -F_0x2e_019024_bit10 -F_0x2e_019024_bit11 -F_0x2e_019024_bit12 -F_0x2e_024_0x2e__0x2e__0x2e__bit_7 -F_0x2e_024_0x2e__0x2e__0x2e__bit_6 -F_0x2e_024_0x2e__0x2e__0x2e__bit_5 -F_0x2e_024_0x2e__0x2e__0x2e__bit_4 -F_0x2e_024_0x2e__0x2e__0x2e__bit_3 -F_0x2e_024_0x2e__0x2e__0x2e__bit_2 -F_0x2e_024_0x2e__0x2e__0x2e__bit_1 F_0x2e_024_0x2e__0x2e__0x2e__bit0 -F_0x2e_024_0x2e__0x2e__0x2e__bit1 -F_0x2e_024_0x2e__0x2e__0x2e__bit2 F_0x2e_024_0x2e__0x2e__0x2e__bit3 -F_0x2e_024_0x2e__0x2e__0x2e__bit4 F_0x2e_024_0x2e__0x2e__0x2e__bit5 -F_0x2e_024_0x2e__0x2e__0x2e__bit6 -F_0x2e_024_0x2e__0x2e__0x2e__bit7 -F_0x2e_024_0x2e__0x2e__0x2e__bit8 -F_0x2e_024_0x2e__0x2e__0x2e__bit9 -F_0x2e_024_0x2e__0x2e__0x2e__bit10 -F_0x2e_024_0x2e__0x2e__0x2e__bit11 -F_0x2e_024_0x2e__0x2e__0x2e__bit12 -F_0x2e_023024_bit_7 -F_0x2e_023024_bit_6 -F_0x2e_023024_bit_5 -F_0x2e_023024_bit_4 -F_0x2e_023024_bit_3 -F_0x2e_023024_bit_2 -F_0x2e_023024_bit_1 -F_0x2e_023024_bit0 -F_0x2e_023024_bit1 -F_0x2e_023024_bit2 -F_0x2e_023024_bit3 -F_0x2e_023024_bit4 -F_0x2e_023024_bit5 -F_0x2e_023024_bit6 -F_0x2e_023024_bit7 -F_0x2e_023024_bit8 -F_0x2e_023024_bit9 -F_0x2e_023024_bit10 -F_0x2e_023024_bit11 -F_0x2e_023024_bit12 -F_0x2e_022023_bit_7 -F_0x2e_022023_bit_6 -F_0x2e_022023_bit_5 -F_0x2e_022023_bit_4 -F_0x2e_022023_bit_3 -F_0x2e_022023_bit_2 -F_0x2e_022023_bit_1 -F_0x2e_022023_bit0 -F_0x2e_022023_bit1 -F_0x2e_022023_bit2 -F_0x2e_022023_bit3 -F_0x2e_022023_bit4 -F_0x2e_022023_bit5 -F_0x2e_022023_bit6 -F_0x2e_022023_bit7 -F_0x2e_022023_bit8 -F_0x2e_022023_bit9 -F_0x2e_022023_bit10 -F_0x2e_022023_bit11 -F_0x2e_022023_bit12 -F_0x2e_020022_bit_7 -F_0x2e_020022_bit_6 -F_0x2e_020022_bit_5 -F_0x2e_020022_bit_4 -F_0x2e_020022_bit_3 -F_0x2e_020022_bit_2 -F_0x2e_020022_bit_1 -F_0x2e_020022_bit0 -F_0x2e_020022_bit1 -F_0x2e_020022_bit2 -F_0x2e_020022_bit3 -F_0x2e_020022_bit4 -F_0x2e_020022_bit5 -F_0x2e_020022_bit6 -F_0x2e_020022_bit7 -F_0x2e_020022_bit8 -F_0x2e_020022_bit9 -F_0x2e_020022_bit10 -F_0x2e_020022_bit11 -F_0x2e_020022_bit12 -F_0x2e_021022_bit_7 -F_0x2e_021022_bit_6 -F_0x2e_021022_bit_5 -F_0x2e_021022_bit_4 -F_0x2e_021022_bit_3 -F_0x2e_021022_bit_2 -F_0x2e_021022_bit_1 F_0x2e_021022_bit0 F_0x2e_021022_bit1 F_0x2e_021022_bit2 -F_0x2e_021022_bit3 -F_0x2e_021022_bit4 -F_0x2e_021022_bit5 -F_0x2e_021022_bit6 -F_0x2e_021022_bit7 -F_0x2e_021022_bit8 -F_0x2e_021022_bit9 -F_0x2e_021022_bit10 -F_0x2e_021022_bit11 -F_0x2e_021022_bit12 -F_0x2e_022_0x2e__0x2e__0x2e__bit_7 -F_0x2e_022_0x2e__0x2e__0x2e__bit_6 -F_0x2e_022_0x2e__0x2e__0x2e__bit_5 -F_0x2e_022_0x2e__0x2e__0x2e__bit_4 -F_0x2e_022_0x2e__0x2e__0x2e__bit_3 -F_0x2e_022_0x2e__0x2e__0x2e__bit_2 -F_0x2e_022_0x2e__0x2e__0x2e__bit_1 F_0x2e_022_0x2e__0x2e__0x2e__bit0 F_0x2e_022_0x2e__0x2e__0x2e__bit1 F_0x2e_022_0x2e__0x2e__0x2e__bit2 -F_0x2e_022_0x2e__0x2e__0x2e__bit3 -F_0x2e_022_0x2e__0x2e__0x2e__bit4 -F_0x2e_022_0x2e__0x2e__0x2e__bit5 -F_0x2e_022_0x2e__0x2e__0x2e__bit6 -F_0x2e_022_0x2e__0x2e__0x2e__bit7 -F_0x2e_022_0x2e__0x2e__0x2e__bit8 -F_0x2e_022_0x2e__0x2e__0x2e__bit9 -F_0x2e_022_0x2e__0x2e__0x2e__bit10 -F_0x2e_022_0x2e__0x2e__0x2e__bit11 -F_0x2e_022_0x2e__0x2e__0x2e__bit12 -F_0x2e_024026_bit_7 -F_0x2e_024026_bit_6 -F_0x2e_024026_bit_5 -F_0x2e_024026_bit_4 -F_0x2e_024026_bit_3 -F_0x2e_024026_bit_2 -F_0x2e_024026_bit_1 -F_0x2e_024026_bit0 -F_0x2e_024026_bit1 -F_0x2e_024026_bit2 -F_0x2e_024026_bit3 -F_0x2e_024026_bit4 -F_0x2e_024026_bit5 -F_0x2e_024026_bit6 -F_0x2e_024026_bit7 -F_0x2e_024026_bit8 -F_0x2e_024026_bit9 -F_0x2e_024026_bit10 -F_0x2e_024026_bit11 -F_0x2e_024026_bit12 -F_0x2e_025026_bit_7 -F_0x2e_025026_bit_6 -F_0x2e_025026_bit_5 -F_0x2e_025026_bit_4 -F_0x2e_025026_bit_3 -F_0x2e_025026_bit_2 -F_0x2e_025026_bit_1 F_0x2e_025026_bit0 F_0x2e_025026_bit1 -F_0x2e_025026_bit2 -F_0x2e_025026_bit3 F_0x2e_025026_bit4 -F_0x2e_025026_bit5 -F_0x2e_025026_bit6 -F_0x2e_025026_bit7 -F_0x2e_025026_bit8 -F_0x2e_025026_bit9 -F_0x2e_025026_bit10 -F_0x2e_025026_bit11 -F_0x2e_025026_bit12 -F_0x2e_025_0x2e__0x2e__0x2e__bit_7 -F_0x2e_025_0x2e__0x2e__0x2e__bit_6 -F_0x2e_025_0x2e__0x2e__0x2e__bit_5 -F_0x2e_025_0x2e__0x2e__0x2e__bit_4 -F_0x2e_025_0x2e__0x2e__0x2e__bit_3 -F_0x2e_025_0x2e__0x2e__0x2e__bit_2 -F_0x2e_025_0x2e__0x2e__0x2e__bit_1 -F_0x2e_025_0x2e__0x2e__0x2e__bit0 -F_0x2e_025_0x2e__0x2e__0x2e__bit1 -F_0x2e_025_0x2e__0x2e__0x2e__bit2 -F_0x2e_025_0x2e__0x2e__0x2e__bit3 -F_0x2e_025_0x2e__0x2e__0x2e__bit4 -F_0x2e_025_0x2e__0x2e__0x2e__bit5 -F_0x2e_025_0x2e__0x2e__0x2e__bit6 -F_0x2e_025_0x2e__0x2e__0x2e__bit7 -F_0x2e_025_0x2e__0x2e__0x2e__bit8 -F_0x2e_025_0x2e__0x2e__0x2e__bit9 -F_0x2e_025_0x2e__0x2e__0x2e__bit10 -F_0x2e_025_0x2e__0x2e__0x2e__bit11 -F_0x2e_025_0x2e__0x2e__0x2e__bit12 -F_0x2e_026027_bit_7 -F_0x2e_026027_bit_6 -F_0x2e_026027_bit_5 -F_0x2e_026027_bit_4 -F_0x2e_026027_bit_3 -F_0x2e_026027_bit_2 -F_0x2e_026027_bit_1 F_0x2e_026027_bit0 -F_0x2e_026027_bit1 F_0x2e_026027_bit2 F_0x2e_026027_bit3 F_0x2e_026027_bit4 -F_0x2e_026027_bit5 -F_0x2e_026027_bit6 -F_0x2e_026027_bit7 -F_0x2e_026027_bit8 -F_0x2e_026027_bit9 -F_0x2e_026027_bit10 -F_0x2e_026027_bit11 -F_0x2e_026027_bit12 -F_0x2e_027_0x2e__0x2e__0x2e__bit_7 -F_0x2e_027_0x2e__0x2e__0x2e__bit_6 -F_0x2e_027_0x2e__0x2e__0x2e__bit_5 -F_0x2e_027_0x2e__0x2e__0x2e__bit_4 -F_0x2e_027_0x2e__0x2e__0x2e__bit_3 -F_0x2e_027_0x2e__0x2e__0x2e__bit_2 -F_0x2e_027_0x2e__0x2e__0x2e__bit_1 F_0x2e_027_0x2e__0x2e__0x2e__bit0 -F_0x2e_027_0x2e__0x2e__0x2e__bit1 F_0x2e_027_0x2e__0x2e__0x2e__bit2 F_0x2e_027_0x2e__0x2e__0x2e__bit3 F_0x2e_027_0x2e__0x2e__0x2e__bit4 -F_0x2e_027_0x2e__0x2e__0x2e__bit5 -F_0x2e_027_0x2e__0x2e__0x2e__bit6 -F_0x2e_027_0x2e__0x2e__0x2e__bit7 -F_0x2e_027_0x2e__0x2e__0x2e__bit8 -F_0x2e_027_0x2e__0x2e__0x2e__bit9 -F_0x2e_027_0x2e__0x2e__0x2e__bit10 -F_0x2e_027_0x2e__0x2e__0x2e__bit11 -F_0x2e_027_0x2e__0x2e__0x2e__bit12 -F_0x2e_027032_bit_7 -F_0x2e_027032_bit_6 -F_0x2e_027032_bit_5 -F_0x2e_027032_bit_4 -F_0x2e_027032_bit_3 -F_0x2e_027032_bit_2 -F_0x2e_027032_bit_1 -F_0x2e_027032_bit0 -F_0x2e_027032_bit1 -F_0x2e_027032_bit2 -F_0x2e_027032_bit3 -F_0x2e_027032_bit4 -F_0x2e_027032_bit5 -F_0x2e_027032_bit6 -F_0x2e_027032_bit7 -F_0x2e_027032_bit8 -F_0x2e_027032_bit9 -F_0x2e_027032_bit10 -F_0x2e_027032_bit11 -F_0x2e_027032_bit12 -F_0x2e_030031_bit_7 -F_0x2e_030031_bit_6 -F_0x2e_030031_bit_5 -F_0x2e_030031_bit_4 -F_0x2e_030031_bit_3 -F_0x2e_030031_bit_2 -F_0x2e_030031_bit_1 -F_0x2e_030031_bit0 -F_0x2e_030031_bit1 -F_0x2e_030031_bit2 -F_0x2e_030031_bit3 -F_0x2e_030031_bit4 -F_0x2e_030031_bit5 -F_0x2e_030031_bit6 -F_0x2e_030031_bit7 -F_0x2e_030031_bit8 -F_0x2e_030031_bit9 -F_0x2e_030031_bit10 -F_0x2e_030031_bit11 -F_0x2e_030031_bit12 -F_0x2e_031032_bit_7 -F_0x2e_031032_bit_6 -F_0x2e_031032_bit_5 -F_0x2e_031032_bit_4 -F_0x2e_031032_bit_3 -F_0x2e_031032_bit_2 -F_0x2e_031032_bit_1 F_0x2e_031032_bit0 -F_0x2e_031032_bit1 F_0x2e_031032_bit2 -F_0x2e_031032_bit3 -F_0x2e_031032_bit4 -F_0x2e_031032_bit5 -F_0x2e_031032_bit6 -F_0x2e_031032_bit7 -F_0x2e_031032_bit8 -F_0x2e_031032_bit9 -F_0x2e_031032_bit10 -F_0x2e_031032_bit11 -F_0x2e_031032_bit12 -F_0x2e_029031_bit_7 -F_0x2e_029031_bit_6 -F_0x2e_029031_bit_5 -F_0x2e_029031_bit_4 -F_0x2e_029031_bit_3 -F_0x2e_029031_bit_2 -F_0x2e_029031_bit_1 F_0x2e_029031_bit0 -F_0x2e_029031_bit1 F_0x2e_029031_bit2 -F_0x2e_029031_bit3 -F_0x2e_029031_bit4 -F_0x2e_029031_bit5 -F_0x2e_029031_bit6 -F_0x2e_029031_bit7 -F_0x2e_029031_bit8 -F_0x2e_029031_bit9 -F_0x2e_029031_bit10 -F_0x2e_029031_bit11 -F_0x2e_029031_bit12 -F_0x2e_028029_bit_7 -F_0x2e_028029_bit_6 -F_0x2e_028029_bit_5 -F_0x2e_028029_bit_4 -F_0x2e_028029_bit_3 -F_0x2e_028029_bit_2 -F_0x2e_028029_bit_1 -F_0x2e_028029_bit0 -F_0x2e_028029_bit1 -F_0x2e_028029_bit2 -F_0x2e_028029_bit3 -F_0x2e_028029_bit4 -F_0x2e_028029_bit5 -F_0x2e_028029_bit6 -F_0x2e_028029_bit7 -F_0x2e_028029_bit8 -F_0x2e_028029_bit9 -F_0x2e_028029_bit10 -F_0x2e_028029_bit11 -F_0x2e_028029_bit12 -F_0x2e_028_0x2e__0x2e__0x2e__bit_7 -F_0x2e_028_0x2e__0x2e__0x2e__bit_6 -F_0x2e_028_0x2e__0x2e__0x2e__bit_5 -F_0x2e_028_0x2e__0x2e__0x2e__bit_4 -F_0x2e_028_0x2e__0x2e__0x2e__bit_3 -F_0x2e_028_0x2e__0x2e__0x2e__bit_2 -F_0x2e_028_0x2e__0x2e__0x2e__bit_1 -F_0x2e_028_0x2e__0x2e__0x2e__bit0 -F_0x2e_028_0x2e__0x2e__0x2e__bit1 -F_0x2e_028_0x2e__0x2e__0x2e__bit2 -F_0x2e_028_0x2e__0x2e__0x2e__bit3 -F_0x2e_028_0x2e__0x2e__0x2e__bit4 -F_0x2e_028_0x2e__0x2e__0x2e__bit5 -F_0x2e_028_0x2e__0x2e__0x2e__bit6 -F_0x2e_028_0x2e__0x2e__0x2e__bit7 -F_0x2e_028_0x2e__0x2e__0x2e__bit8 -F_0x2e_028_0x2e__0x2e__0x2e__bit9 -F_0x2e_028_0x2e__0x2e__0x2e__bit10 -F_0x2e_028_0x2e__0x2e__0x2e__bit11 -F_0x2e_028_0x2e__0x2e__0x2e__bit12 -F_0x2e_032033_bit_7 -F_0x2e_032033_bit_6 -F_0x2e_032033_bit_5 -F_0x2e_032033_bit_4 -F_0x2e_032033_bit_3 -F_0x2e_032033_bit_2 -F_0x2e_032033_bit_1 F_0x2e_032033_bit0 -F_0x2e_032033_bit1 F_0x2e_032033_bit2 -F_0x2e_032033_bit3 -F_0x2e_032033_bit4 -F_0x2e_032033_bit5 -F_0x2e_032033_bit6 -F_0x2e_032033_bit7 -F_0x2e_032033_bit8 -F_0x2e_032033_bit9 -F_0x2e_032033_bit10 -F_0x2e_032033_bit11 -F_0x2e_032033_bit12 -F_0x2e_033037_bit_7 -F_0x2e_033037_bit_6 -F_0x2e_033037_bit_5 -F_0x2e_033037_bit_4 -F_0x2e_033037_bit_3 -F_0x2e_033037_bit_2 -F_0x2e_033037_bit_1 F_0x2e_033037_bit0 -F_0x2e_033037_bit1 F_0x2e_033037_bit2 -F_0x2e_033037_bit3 -F_0x2e_033037_bit4 -F_0x2e_033037_bit5 -F_0x2e_033037_bit6 -F_0x2e_033037_bit7 -F_0x2e_033037_bit8 -F_0x2e_033037_bit9 -F_0x2e_033037_bit10 -F_0x2e_033037_bit11 -F_0x2e_033037_bit12 -F_0x2e_034036_bit_7 -F_0x2e_034036_bit_6 -F_0x2e_034036_bit_5 -F_0x2e_034036_bit_4 -F_0x2e_034036_bit_3 -F_0x2e_034036_bit_2 -F_0x2e_034036_bit_1 -F_0x2e_034036_bit0 -F_0x2e_034036_bit1 -F_0x2e_034036_bit2 -F_0x2e_034036_bit3 -F_0x2e_034036_bit4 -F_0x2e_034036_bit5 -F_0x2e_034036_bit6 -F_0x2e_034036_bit7 -F_0x2e_034036_bit8 -F_0x2e_034036_bit9 -F_0x2e_034036_bit10 -F_0x2e_034036_bit11 -F_0x2e_034036_bit12 -F_0x2e_035036_bit_7 -F_0x2e_035036_bit_6 -F_0x2e_035036_bit_5 -F_0x2e_035036_bit_4 -F_0x2e_035036_bit_3 -F_0x2e_035036_bit_2 -F_0x2e_035036_bit_1 -F_0x2e_035036_bit0 -F_0x2e_035036_bit1 -F_0x2e_035036_bit2 -F_0x2e_035036_bit3 -F_0x2e_035036_bit4 -F_0x2e_035036_bit5 -F_0x2e_035036_bit6 -F_0x2e_035036_bit7 -F_0x2e_035036_bit8 -F_0x2e_035036_bit9 -F_0x2e_035036_bit10 -F_0x2e_035036_bit11 -F_0x2e_035036_bit12 -F_0x2e_037038_bit_7 -F_0x2e_037038_bit_6 -F_0x2e_037038_bit_5 -F_0x2e_037038_bit_4 -F_0x2e_037038_bit_3 -F_0x2e_037038_bit_2 -F_0x2e_037038_bit_1 F_0x2e_037038_bit0 -F_0x2e_037038_bit1 F_0x2e_037038_bit2 -F_0x2e_037038_bit3 -F_0x2e_037038_bit4 -F_0x2e_037038_bit5 -F_0x2e_037038_bit6 -F_0x2e_037038_bit7 -F_0x2e_037038_bit8 -F_0x2e_037038_bit9 -F_0x2e_037038_bit10 -F_0x2e_037038_bit11 -F_0x2e_037038_bit12 -F_0x2e_039040_bit_7 -F_0x2e_039040_bit_6 -F_0x2e_039040_bit_5 -F_0x2e_039040_bit_4 -F_0x2e_039040_bit_3 -F_0x2e_039040_bit_2 -F_0x2e_039040_bit_1 F_0x2e_039040_bit0 -F_0x2e_039040_bit1 F_0x2e_039040_bit2 -F_0x2e_039040_bit3 -F_0x2e_039040_bit4 -F_0x2e_039040_bit5 -F_0x2e_039040_bit6 -F_0x2e_039040_bit7 -F_0x2e_039040_bit8 -F_0x2e_039040_bit9 -F_0x2e_039040_bit10 -F_0x2e_039040_bit11 -F_0x2e_039040_bit12 -F_0x2e_040_0x2e__0x2e__0x2e__bit_7 -F_0x2e_040_0x2e__0x2e__0x2e__bit_6 -F_0x2e_040_0x2e__0x2e__0x2e__bit_5 -F_0x2e_040_0x2e__0x2e__0x2e__bit_4 -F_0x2e_040_0x2e__0x2e__0x2e__bit_3 -F_0x2e_040_0x2e__0x2e__0x2e__bit_2 -F_0x2e_040_0x2e__0x2e__0x2e__bit_1 -F_0x2e_040_0x2e__0x2e__0x2e__bit0 -F_0x2e_040_0x2e__0x2e__0x2e__bit1 -F_0x2e_040_0x2e__0x2e__0x2e__bit2 -F_0x2e_040_0x2e__0x2e__0x2e__bit3 -F_0x2e_040_0x2e__0x2e__0x2e__bit4 -F_0x2e_040_0x2e__0x2e__0x2e__bit5 -F_0x2e_040_0x2e__0x2e__0x2e__bit6 -F_0x2e_040_0x2e__0x2e__0x2e__bit7 -F_0x2e_040_0x2e__0x2e__0x2e__bit8 -F_0x2e_040_0x2e__0x2e__0x2e__bit9 -F_0x2e_040_0x2e__0x2e__0x2e__bit10 -F_0x2e_040_0x2e__0x2e__0x2e__bit11 -F_0x2e_040_0x2e__0x2e__0x2e__bit12 -F_0x2e_041_0x2e__0x2e__0x2e__bit_7 -F_0x2e_041#### 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.95 0.90 2/54 25907 Raw data (stat): 25907 (runsolver) R 25906 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542623297 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s] Raw data (loadavg): 0.87 0.95 0.90 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 8235 0 0 0 980 17 0 0 25 0 1 0 542623297 37789696 7894 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9226 7894 603 41 0 9185 0 vsize: 36904 [startup+20.0005 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 12833 0 0 0 1970 27 0 0 25 0 1 0 542623297 62193664 12492 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15184 12492 603 41 0 15143 0 vsize: 60736 [startup+30.0005 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 12977 0 0 0 2969 28 0 0 25 0 1 0 542623297 62242816 12636 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15196 12636 603 41 0 15155 0 vsize: 60784 [startup+40.0002 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 17654 0 0 0 3958 40 0 0 25 0 1 0 542623297 77312000 16983 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18875 16983 603 41 0 18834 0 vsize: 75500 [startup+50.0006 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 17779 0 0 0 4958 40 0 0 25 0 1 0 542623297 78094336 17108 4294967295 134512640 134672761 3221224544 3221221244 134544678 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19066 17108 603 41 0 19025 0 vsize: 76264 [startup+60.0009 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 17824 0 0 0 5958 40 0 0 25 0 1 0 542623297 78204928 17153 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19093 17153 603 41 0 19052 0 vsize: 76372 [startup+70.0014 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 21050 0 0 0 6951 47 0 0 25 0 1 0 542623297 92475392 20379 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22577 20379 603 41 0 22536 0 vsize: 90308 [startup+80.0017 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 21099 0 0 0 7951 47 0 0 25 0 1 0 542623297 92758016 20428 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22646 20428 603 41 0 22605 0 vsize: 90584 [startup+90.0017 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 21230 0 0 0 8951 47 0 0 25 0 1 0 542623297 92876800 20559 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22675 20559 603 41 0 22634 0 vsize: 90700 [startup+100.002 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 21250 0 0 0 9951 47 0 0 25 0 1 0 542623297 93011968 20579 4294967295 134512640 134672761 3221224544 3221223696 1074743887 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22708 20579 603 41 0 22667 0 vsize: 90832 [startup+110.002 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 21280 0 0 0 10951 47 0 0 25 0 1 0 542623297 93143040 20609 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22740 20609 603 41 0 22699 0 vsize: 90960 [startup+120.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 23999 0 0 0 11943 56 0 0 25 0 1 0 542623297 117370880 23328 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28655 23328 603 41 0 28614 0 vsize: 114620 [startup+130.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 23999 0 0 0 12943 56 0 0 25 0 1 0 542623297 117370880 23328 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28655 23328 603 41 0 28614 0 vsize: 114620 [startup+140.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24019 0 0 0 13943 56 0 0 25 0 1 0 542623297 117370880 23348 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28655 23348 603 41 0 28614 0 vsize: 114620 [startup+150.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24060 0 0 0 14943 56 0 0 25 0 1 0 542623297 117641216 23389 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28721 23389 603 41 0 28680 0 vsize: 114884 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24125 0 0 0 15943 56 0 0 25 0 1 0 542623297 117866496 23454 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28776 23454 603 41 0 28735 0 vsize: 115104 [startup+170.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24126 0 0 0 16943 56 0 0 25 0 1 0 542623297 117866496 23455 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28776 23455 603 41 0 28735 0 vsize: 115104 [startup+180.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24132 0 0 0 17943 56 0 0 25 0 1 0 542623297 117866496 23461 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28776 23461 603 41 0 28735 0 vsize: 115104 [startup+190.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24169 0 0 0 18944 56 0 0 25 0 1 0 542623297 117964800 23498 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28800 23498 603 41 0 28759 0 vsize: 115200 [startup+200.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24178 0 0 0 19944 56 0 0 25 0 1 0 542623297 118009856 23507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28811 23507 603 41 0 28770 0 vsize: 115244 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24191 0 0 0 20944 56 0 0 25 0 1 0 542623297 118063104 23520 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28824 23520 603 41 0 28783 0 vsize: 115296 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24193 0 0 0 21944 57 0 0 25 0 1 0 542623297 118063104 23522 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28824 23522 603 41 0 28783 0 vsize: 115296 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24216 0 0 0 22944 57 0 0 25 0 1 0 542623297 118153216 23545 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28846 23545 603 41 0 28805 0 vsize: 115384 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24227 0 0 0 23944 57 0 0 25 0 1 0 542623297 118185984 23556 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28854 23556 603 41 0 28813 0 vsize: 115416 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24232 0 0 0 24944 57 0 0 25 0 1 0 542623297 118190080 23561 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28855 23561 603 41 0 28814 0 vsize: 115420 [startup+260.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24232 0 0 0 25944 58 0 0 25 0 1 0 542623297 118190080 23561 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28855 23561 603 41 0 28814 0 vsize: 115420 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24232 0 0 0 26944 58 0 0 25 0 1 0 542623297 118190080 23561 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28855 23561 603 41 0 28814 0 vsize: 115420 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24238 0 0 0 27944 58 0 0 25 0 1 0 542623297 118325248 23567 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28888 23567 603 41 0 28847 0 vsize: 115552 [startup+290.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24245 0 0 0 28944 58 0 0 25 0 1 0 542623297 118325248 23574 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28888 23574 603 41 0 28847 0 vsize: 115552 [startup+300.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24287 0 0 0 29943 58 0 0 25 0 1 0 542623297 118427648 23616 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+310.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24287 0 0 0 30943 58 0 0 25 0 1 0 542623297 118427648 23616 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+320.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24287 0 0 0 31944 58 0 0 25 0 1 0 542623297 118427648 23616 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+330.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24287 0 0 0 32944 58 0 0 25 0 1 0 542623297 118427648 23616 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+340.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24309 0 0 0 33944 59 0 0 25 0 1 0 542623297 118681600 23638 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28975 23638 603 41 0 28934 0 vsize: 115900 [startup+350.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24309 0 0 0 34944 59 0 0 25 0 1 0 542623297 118681600 23638 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28975 23638 603 41 0 28934 0 vsize: 115900 [startup+360.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24309 0 0 0 35944 59 0 0 25 0 1 0 542623297 118681600 23638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28975 23638 603 41 0 28934 0 vsize: 115900 [startup+370.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24314 0 0 0 36944 59 0 0 25 0 1 0 542623297 118681600 23643 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28975 23643 603 41 0 28934 0 vsize: 115900 [startup+380.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24320 0 0 0 37945 59 0 0 25 0 1 0 542623297 118681600 23649 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28975 23649 603 41 0 28934 0 vsize: 115900 [startup+390.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24360 0 0 0 38945 59 0 0 25 0 1 0 542623297 118759424 23689 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28994 23689 603 41 0 28953 0 vsize: 115976 [startup+400.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24361 0 0 0 39945 59 0 0 25 0 1 0 542623297 118902784 23690 4294967295 134512640 134672761 3221224544 3221223728 134558513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29029 23690 603 41 0 28988 0 vsize: 116116 [startup+410.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24361 0 0 0 40945 59 0 0 25 0 1 0 542623297 118902784 23690 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29029 23690 603 41 0 28988 0 vsize: 116116 [startup+420.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24372 0 0 0 41945 59 0 0 25 0 1 0 542623297 118902784 23701 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29029 23701 603 41 0 28988 0 vsize: 116116 [startup+430.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24379 0 0 0 42945 59 0 0 25 0 1 0 542623297 118902784 23708 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29029 23708 603 41 0 28988 0 vsize: 116116 [startup+440.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24383 0 0 0 43945 59 0 0 25 0 1 0 542623297 118902784 23712 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29029 23712 603 41 0 28988 0 vsize: 116116 [startup+450.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24393 0 0 0 44945 59 0 0 25 0 1 0 542623297 118902784 23722 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29029 23722 603 41 0 28988 0 vsize: 116116 [startup+460.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24400 0 0 0 45946 59 0 0 25 0 1 0 542623297 119037952 23729 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29062 23729 603 41 0 29021 0 vsize: 116248 [startup+470.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24404 0 0 0 46946 59 0 0 25 0 1 0 542623297 119037952 23733 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29062 23733 603 41 0 29021 0 vsize: 116248 [startup+480.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24406 0 0 0 47946 59 0 0 25 0 1 0 542623297 119037952 23735 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29062 23735 603 41 0 29021 0 vsize: 116248 [startup+490.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24417 0 0 0 48945 59 0 0 25 0 1 0 542623297 119037952 23746 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29062 23746 603 41 0 29021 0 vsize: 116248 [startup+500.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24425 0 0 0 49945 59 0 0 25 0 1 0 542623297 119037952 23754 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29062 23754 603 41 0 29021 0 vsize: 116248 [startup+510.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24435 0 0 0 50945 59 0 0 25 0 1 0 542623297 119169024 23764 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29094 23764 603 41 0 29053 0 vsize: 116376 [startup+520.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24512 0 0 0 51946 60 0 0 25 0 1 0 542623297 119566336 23841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29191 23841 603 41 0 29150 0 vsize: 116764 [startup+530.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24514 0 0 0 52945 60 0 0 25 0 1 0 542623297 119566336 23843 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29191 23843 603 41 0 29150 0 vsize: 116764 [startup+540.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24531 0 0 0 53945 60 0 0 25 0 1 0 542623297 119566336 23860 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29191 23860 603 41 0 29150 0 vsize: 116764 [startup+550.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24536 0 0 0 54946 60 0 0 25 0 1 0 542623297 119640064 23865 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29209 23865 603 41 0 29168 0 vsize: 116836 [startup+560.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24544 0 0 0 55946 60 0 0 25 0 1 0 542623297 119640064 23873 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29209 23873 603 41 0 29168 0 vsize: 116836 [startup+570.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24547 0 0 0 56946 60 0 0 25 0 1 0 542623297 119640064 23876 4294967295 134512640 134672761 3221224544 3221222960 134597195 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29209 23876 603 41 0 29168 0 vsize: 116836 [startup+580.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24548 0 0 0 57946 60 0 0 25 0 1 0 542623297 119640064 23877 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29209 23877 603 41 0 29168 0 vsize: 116836 [startup+590.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24548 0 0 0 58946 60 0 0 25 0 1 0 542623297 119640064 23877 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29209 23877 603 41 0 29168 0 vsize: 116836 [startup+600.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24549 0 0 0 59946 60 0 0 25 0 1 0 542623297 119640064 23878 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29209 23878 603 41 0 29168 0 vsize: 116836 [startup+610.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24559 0 0 0 60947 60 0 0 25 0 1 0 542623297 119771136 23888 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29241 23888 603 41 0 29200 0 vsize: 116964 [startup+620.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24574 0 0 0 61947 60 0 0 25 0 1 0 542623297 119771136 23903 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29241 23903 603 41 0 29200 0 vsize: 116964 [startup+630.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24589 0 0 0 62947 60 0 0 25 0 1 0 542623297 119771136 23918 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29241 23918 603 41 0 29200 0 vsize: 116964 [startup+640.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24604 0 0 0 63947 60 0 0 25 0 1 0 542623297 119910400 23933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29275 23933 603 41 0 29234 0 vsize: 117100 [startup+650.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24615 0 0 0 64947 60 0 0 25 0 1 0 542623297 119910400 23944 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29275 23944 603 41 0 29234 0 vsize: 117100 [startup+660.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24621 0 0 0 65947 60 0 0 25 0 1 0 542623297 119910400 23950 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29275 23950 603 41 0 29234 0 vsize: 117100 [startup+670.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24632 0 0 0 66948 60 0 0 25 0 1 0 542623297 120045568 23961 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29308 23961 603 41 0 29267 0 vsize: 117232 [startup+680.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24640 0 0 0 67948 60 0 0 25 0 1 0 542623297 120045568 23969 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29308 23969 603 41 0 29267 0 vsize: 117232 [startup+690.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24650 0 0 0 68948 60 0 0 25 0 1 0 542623297 120045568 23979 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29308 23979 603 41 0 29267 0 vsize: 117232 [startup+700.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24660 0 0 0 69948 60 0 0 25 0 1 0 542623297 120168448 23989 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29338 23989 603 41 0 29297 0 vsize: 117352 [startup+710.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24667 0 0 0 70948 60 0 0 25 0 1 0 542623297 120168448 23996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29338 23996 603 41 0 29297 0 vsize: 117352 [startup+720.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24699 0 0 0 71948 61 0 0 25 0 1 0 542623297 120213504 24028 4294967295 134512640 134672761 3221224544 3221221376 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29349 24028 603 41 0 29308 0 vsize: 117396 [startup+730.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24718 0 0 0 72949 61 0 0 25 0 1 0 542623297 120279040 24047 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29365 24047 603 41 0 29324 0 vsize: 117460 [startup+740.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24718 0 0 0 73949 61 0 0 25 0 1 0 542623297 120279040 24047 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29365 24047 603 41 0 29324 0 vsize: 117460 [startup+750.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24718 0 0 0 74949 61 0 0 25 0 1 0 542623297 120279040 24047 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29365 24047 603 41 0 29324 0 vsize: 117460 [startup+760.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24729 0 0 0 75949 61 0 0 25 0 1 0 542623297 120406016 24058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29396 24058 603 41 0 29355 0 vsize: 117584 [startup+770.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24739 0 0 0 76949 61 0 0 25 0 1 0 542623297 120406016 24068 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29396 24068 603 41 0 29355 0 vsize: 117584 [startup+780.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24757 0 0 0 77949 61 0 0 25 0 1 0 542623297 120532992 24086 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29427 24086 603 41 0 29386 0 vsize: 117708 [startup+790.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24767 0 0 0 78949 61 0 0 25 0 1 0 542623297 120532992 24096 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29427 24096 603 41 0 29386 0 vsize: 117708 [startup+800.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24774 0 0 0 79950 61 0 0 25 0 1 0 542623297 120532992 24103 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29427 24103 603 41 0 29386 0 vsize: 117708 [startup+810.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24781 0 0 0 80950 61 0 0 25 0 1 0 542623297 120532992 24110 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29427 24110 603 41 0 29386 0 vsize: 117708 [startup+820.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24790 0 0 0 81950 61 0 0 25 0 1 0 542623297 120664064 24119 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29459 24119 603 41 0 29418 0 vsize: 117836 [startup+830.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24806 0 0 0 82950 61 0 0 25 0 1 0 542623297 120664064 24135 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29459 24135 603 41 0 29418 0 vsize: 117836 [startup+840.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24821 0 0 0 83950 61 0 0 25 0 1 0 542623297 120786944 24150 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29489 24150 603 41 0 29448 0 vsize: 117956 [startup+850.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24833 0 0 0 84950 62 0 0 25 0 1 0 542623297 120786944 24162 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29489 24162 603 41 0 29448 0 vsize: 117956 [startup+860.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24848 0 0 0 85950 62 0 0 25 0 1 0 542623297 120918016 24177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29521 24177 603 41 0 29480 0 vsize: 118084 [startup+870.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24858 0 0 0 86950 62 0 0 25 0 1 0 542623297 120918016 24187 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29521 24187 603 41 0 29480 0 vsize: 118084 [startup+880.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24869 0 0 0 87950 62 0 0 25 0 1 0 542623297 120918016 24198 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29521 24198 603 41 0 29480 0 vsize: 118084 [startup+890.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24877 0 0 0 88950 62 0 0 25 0 1 0 542623297 121044992 24206 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29552 24206 603 41 0 29511 0 vsize: 118208 [startup+900.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24884 0 0 0 89950 62 0 0 25 0 1 0 542623297 121044992 24213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29552 24213 603 41 0 29511 0 vsize: 118208 [startup+910.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24897 0 0 0 90950 63 0 0 25 0 1 0 542623297 121044992 24226 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29552 24226 603 41 0 29511 0 vsize: 118208 [startup+920.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24905 0 0 0 91950 63 0 0 25 0 1 0 542623297 121044992 24234 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29552 24234 603 41 0 29511 0 vsize: 118208 [startup+930.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24938 0 0 0 92950 63 0 0 25 0 1 0 542623297 121171968 24267 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29583 24267 603 41 0 29542 0 vsize: 118332 [startup+940.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24938 0 0 0 93950 63 0 0 25 0 1 0 542623297 121171968 24267 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29583 24267 603 41 0 29542 0 vsize: 118332 [startup+950.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24944 0 0 0 94950 63 0 0 25 0 1 0 542623297 121307136 24273 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29616 24273 603 41 0 29575 0 vsize: 118464 [startup+960.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24951 0 0 0 95951 63 0 0 25 0 1 0 542623297 121307136 24280 4294967295 134512640 134672761 3221224544 3221223680 134560625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29616 24280 603 41 0 29575 0 vsize: 118464 [startup+970.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24959 0 0 0 96951 63 0 0 25 0 1 0 542623297 121307136 24288 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29616 24288 603 41 0 29575 0 vsize: 118464 [startup+980.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24974 0 0 0 97951 63 0 0 25 0 1 0 542623297 121438208 24303 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29648 24303 603 41 0 29607 0 vsize: 118592 [startup+990.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 24988 0 0 0 98951 63 0 0 25 0 1 0 542623297 121438208 24317 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29648 24317 603 41 0 29607 0 vsize: 118592 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25012 0 0 0 99951 63 0 0 25 0 1 0 542623297 121565184 24341 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29679 24341 603 41 0 29638 0 vsize: 118716 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25034 0 0 0 100951 63 0 0 25 0 1 0 542623297 121565184 24363 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29679 24363 603 41 0 29638 0 vsize: 118716 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25047 0 0 0 101951 63 0 0 25 0 1 0 542623297 121696256 24376 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29711 24376 603 41 0 29670 0 vsize: 118844 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25056 0 0 0 102951 63 0 0 25 0 1 0 542623297 121696256 24385 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29711 24385 603 41 0 29670 0 vsize: 118844 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25071 0 0 0 103951 63 0 0 25 0 1 0 542623297 121819136 24400 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29741 24400 603 41 0 29700 0 vsize: 118964 [startup+1050.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25080 0 0 0 104952 63 0 0 25 0 1 0 542623297 121819136 24409 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29741 24409 603 41 0 29700 0 vsize: 118964 [startup+1060.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25090 0 0 0 105952 63 0 0 25 0 1 0 542623297 121819136 24419 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29741 24419 603 41 0 29700 0 vsize: 118964 [startup+1070.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25103 0 0 0 106952 63 0 0 25 0 1 0 542623297 121950208 24432 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29773 24432 603 41 0 29732 0 vsize: 119092 [startup+1080.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25114 0 0 0 107952 64 0 0 25 0 1 0 542623297 121950208 24443 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29773 24443 603 41 0 29732 0 vsize: 119092 [startup+1090.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25123 0 0 0 108952 64 0 0 25 0 1 0 542623297 121950208 24452 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29773 24452 603 41 0 29732 0 vsize: 119092 [startup+1100.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25139 0 0 0 109952 64 0 0 25 0 1 0 542623297 122085376 24468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29806 24468 603 41 0 29765 0 vsize: 119224 [startup+1110.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25154 0 0 0 110952 64 0 0 25 0 1 0 542623297 122085376 24483 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29806 24483 603 41 0 29765 0 vsize: 119224 [startup+1120.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25167 0 0 0 111953 64 0 0 25 0 1 0 542623297 122220544 24496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29839 24496 603 41 0 29798 0 vsize: 119356 [startup+1130.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25182 0 0 0 112953 64 0 0 25 0 1 0 542623297 122220544 24511 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29839 24511 603 41 0 29798 0 vsize: 119356 [startup+1140.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25192 0 0 0 113953 64 0 0 25 0 1 0 542623297 122220544 24521 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29839 24521 603 41 0 29798 0 vsize: 119356 [startup+1150.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25204 0 0 0 114953 64 0 0 25 0 1 0 542623297 122351616 24533 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29871 24533 603 41 0 29830 0 vsize: 119484 [startup+1160.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25217 0 0 0 115953 64 0 0 25 0 1 0 542623297 122351616 24546 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29871 24546 603 41 0 29830 0 vsize: 119484 [startup+1170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25228 0 0 0 116953 64 0 0 25 0 1 0 542623297 122351616 24557 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29871 24557 603 41 0 29830 0 vsize: 119484 [startup+1180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25235 0 0 0 117954 64 0 0 25 0 1 0 542623297 122486784 24564 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29904 24564 603 41 0 29863 0 vsize: 119616 [startup+1190.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25244 0 0 0 118954 64 0 0 25 0 1 0 542623297 122486784 24573 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29904 24573 603 41 0 29863 0 vsize: 119616 [startup+1200.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25907 Raw data (stat): 25907 (minisat+) R 25906 28546 28545 0 -1 0 25262 0 0 0 119954 64 0 0 25 0 1 0 542623297 122613760 24591 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29935 24591 603 41 0 29894 0 vsize: 119740 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 25907 Raw data (stat): 25907 (minisat+) Z 25906 28546 28545 0 -1 12 25265 0 0 0 119954 69 0 0 25 0 1 0 542623297 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.08 CPU time (s): 1200.24 CPU user time (s): 1199.55 CPU system time (s): 0.695894 CPU usage (%): 100.014 Max. virtual memory (Kb): 119740 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####