Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-egout.opb |
MD5SUM | fd101f0ba1a3813e843a38997ab7ed84 |
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.04984 |
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 wulflinc18 THE 2005-04-21 15:33:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18303 boxname=wulflinc18 idbench=1408 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fd101f0ba1a3813e843a38997ab7ed84 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-egout.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-egout.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-egout.opb IDLAUNCH: 18303 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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: 830340 kB Buffers: 20408 kB Cached: 160944 kB SwapCached: 752 kB Active: 41360 kB Inactive: 142016 kB HighTotal: 131008 kB HighFree: 5656 kB LowTotal: 903652 kB LowFree: 824684 kB SwapTotal: 2097892 kB SwapFree: 2096168 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5104 kB Slab: 15372 kB Committed_AS: 63816 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 15:53:57 (client local time) WITH STATUS 10 IN 1200.77 SECONDS stats: 18303 7 1200.77 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.91 0.95 0.90 2/55 898 Raw data (stat): 898 (runsolver) R 897 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546185186 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 8235 0 0 0 979 19 0 0 25 0 1 0 546185186 37789696 7894 4294967295 134512640 134672761 3221224544 3221223680 134560611 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.0006 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 12833 0 0 0 1968 29 0 0 25 0 1 0 546185186 62193664 12492 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15184 12492 603 41 0 15143 0 vsize: 60736 [startup+30.0014 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 12977 0 0 0 2968 29 0 0 25 0 1 0 546185186 62242816 12636 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15196 12636 603 41 0 15155 0 vsize: 60784 [startup+40.001 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 17659 0 0 0 3957 40 0 0 25 0 1 0 546185186 77312000 16988 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18875 16988 603 41 0 18834 0 vsize: 75500 [startup+50.021 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 17790 0 0 0 4959 40 0 0 25 0 1 0 546185186 78094336 17119 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19066 17119 603 41 0 19025 0 vsize: 76264 [startup+60.0266 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 17824 0 0 0 5959 40 0 0 25 0 1 0 546185186 78204928 17153 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19093 17153 603 41 0 19052 0 vsize: 76372 [startup+70.0337 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 21059 0 0 0 6951 49 0 0 25 0 1 0 546185186 92610560 20388 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22610 20388 603 41 0 22569 0 vsize: 90440 [startup+80.035 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 21102 0 0 0 7951 49 0 0 25 0 1 0 546185186 92758016 20431 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22646 20431 603 41 0 22605 0 vsize: 90584 [startup+90.0346 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 21231 0 0 0 8951 50 0 0 25 0 1 0 546185186 92876800 20560 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22675 20560 603 41 0 22634 0 vsize: 90700 [startup+100.035 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 898 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 21253 0 0 0 9951 50 0 0 25 0 1 0 546185186 93011968 20582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22708 20582 603 41 0 22667 0 vsize: 90832 [startup+110.036 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 21314 0 0 0 10952 50 0 0 25 0 1 0 546185186 93323264 20643 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22784 20643 603 41 0 22743 0 vsize: 91136 [startup+120.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 23999 0 0 0 11946 56 0 0 25 0 1 0 546185186 117370880 23328 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28655 23328 603 41 0 28614 0 vsize: 114620 [startup+130.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24002 0 0 0 12946 56 0 0 25 0 1 0 546185186 117370880 23331 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28655 23331 603 41 0 28614 0 vsize: 114620 [startup+140.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24034 0 0 0 13946 56 0 0 25 0 1 0 546185186 117506048 23363 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28688 23363 603 41 0 28647 0 vsize: 114752 [startup+150.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24106 0 0 0 14946 56 0 0 25 0 1 0 546185186 117731328 23435 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28743 23435 603 41 0 28702 0 vsize: 114972 [startup+160.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24125 0 0 0 15946 56 0 0 25 0 1 0 546185186 117866496 23454 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28776 23454 603 41 0 28735 0 vsize: 115104 [startup+170.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24129 0 0 0 16946 56 0 0 25 0 1 0 546185186 117866496 23458 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28776 23458 603 41 0 28735 0 vsize: 115104 [startup+180.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24135 0 0 0 17946 56 0 0 25 0 1 0 546185186 117866496 23464 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28776 23464 603 41 0 28735 0 vsize: 115104 [startup+190.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24169 0 0 0 18946 56 0 0 25 0 1 0 546185186 117964800 23498 4294967295 134512640 134672761 3221224544 3221223104 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28800 23498 603 41 0 28759 0 vsize: 115200 [startup+200.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24186 0 0 0 19946 57 0 0 25 0 1 0 546185186 118030336 23515 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28816 23515 603 41 0 28775 0 vsize: 115264 [startup+210.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24193 0 0 0 20947 57 0 0 25 0 1 0 546185186 118063104 23522 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28824 23522 603 41 0 28783 0 vsize: 115296 [startup+220.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24216 0 0 0 21947 57 0 0 25 0 1 0 546185186 118153216 23545 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28846 23545 603 41 0 28805 0 vsize: 115384 [startup+230.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24227 0 0 0 22947 57 0 0 25 0 1 0 546185186 118185984 23556 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28854 23556 603 41 0 28813 0 vsize: 115416 [startup+240.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24232 0 0 0 23947 57 0 0 25 0 1 0 546185186 118190080 23561 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28855 23561 603 41 0 28814 0 vsize: 115420 [startup+250.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24232 0 0 0 24947 57 0 0 25 0 1 0 546185186 118190080 23561 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28855 23561 603 41 0 28814 0 vsize: 115420 [startup+260.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24232 0 0 0 25947 57 0 0 25 0 1 0 546185186 118190080 23561 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28855 23561 603 41 0 28814 0 vsize: 115420 [startup+270.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24237 0 0 0 26947 57 0 0 25 0 1 0 546185186 118325248 23566 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28888 23566 603 41 0 28847 0 vsize: 115552 [startup+280.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24245 0 0 0 27947 57 0 0 25 0 1 0 546185186 118325248 23574 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28888 23574 603 41 0 28847 0 vsize: 115552 [startup+290.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24287 0 0 0 28947 57 0 0 25 0 1 0 546185186 118427648 23616 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+300.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24287 0 0 0 29948 57 0 0 25 0 1 0 546185186 118427648 23616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+310.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24287 0 0 0 30948 57 0 0 25 0 1 0 546185186 118427648 23616 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+320.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24287 0 0 0 31948 57 0 0 25 0 1 0 546185186 118427648 23616 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28913 23616 603 41 0 28872 0 vsize: 115652 [startup+330.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24309 0 0 0 32948 57 0 0 25 0 1 0 546185186 118681600 23638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28975 23638 603 41 0 28934 0 vsize: 115900 [startup+340.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24309 0 0 0 33948 57 0 0 25 0 1 0 546185186 118681600 23638 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28975 23638 603 41 0 28934 0 vsize: 115900 [startup+350.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24309 0 0 0 34948 57 0 0 25 0 1 0 546185186 118681600 23638 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28975 23638 603 41 0 28934 0 vsize: 115900 [startup+360.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24314 0 0 0 35949 57 0 0 25 0 1 0 546185186 118681600 23643 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28975 23643 603 41 0 28934 0 vsize: 115900 [startup+370.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24321 0 0 0 36949 57 0 0 25 0 1 0 546185186 118681600 23650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28975 23650 603 41 0 28934 0 vsize: 115900 [startup+380.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24360 0 0 0 37949 57 0 0 25 0 1 0 546185186 118759424 23689 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28994 23689 603 41 0 28953 0 vsize: 115976 [startup+390.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24361 0 0 0 38949 57 0 0 25 0 1 0 546185186 118902784 23690 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29029 23690 603 41 0 28988 0 vsize: 116116 [startup+400.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 900 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24363 0 0 0 39949 57 0 0 25 0 1 0 546185186 118902784 23692 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29029 23692 603 41 0 28988 0 vsize: 116116 [startup+410.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24374 0 0 0 40949 57 0 0 25 0 1 0 546185186 118902784 23703 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29029 23703 603 41 0 28988 0 vsize: 116116 [startup+420.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24379 0 0 0 41950 57 0 0 25 0 1 0 546185186 118902784 23708 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29029 23708 603 41 0 28988 0 vsize: 116116 [startup+430.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24385 0 0 0 42950 57 0 0 25 0 1 0 546185186 118902784 23714 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29029 23714 603 41 0 28988 0 vsize: 116116 [startup+440.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24396 0 0 0 43950 58 0 0 25 0 1 0 546185186 119037952 23725 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29062 23725 603 41 0 29021 0 vsize: 116248 [startup+450.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24403 0 0 0 44950 58 0 0 25 0 1 0 546185186 119037952 23732 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29062 23732 603 41 0 29021 0 vsize: 116248 [startup+460.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24404 0 0 0 45950 58 0 0 25 0 1 0 546185186 119037952 23733 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29062 23733 603 41 0 29021 0 vsize: 116248 [startup+470.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24412 0 0 0 46950 58 0 0 25 0 1 0 546185186 119037952 23741 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29062 23741 603 41 0 29021 0 vsize: 116248 [startup+480.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24421 0 0 0 47951 58 0 0 25 0 1 0 546185186 119037952 23750 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29062 23750 603 41 0 29021 0 vsize: 116248 [startup+490.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24429 0 0 0 48951 58 0 0 25 0 1 0 546185186 119169024 23758 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29094 23758 603 41 0 29053 0 vsize: 116376 [startup+500.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24445 0 0 0 49951 58 0 0 25 0 1 0 546185186 119169024 23774 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29094 23774 603 41 0 29053 0 vsize: 116376 [startup+510.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24514 0 0 0 50951 58 0 0 25 0 1 0 546185186 119566336 23843 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29191 23843 603 41 0 29150 0 vsize: 116764 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24514 0 0 0 51951 58 0 0 25 0 1 0 546185186 119566336 23843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29191 23843 603 41 0 29150 0 vsize: 116764 [startup+530.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24536 0 0 0 52952 58 0 0 25 0 1 0 546185186 119640064 23865 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29209 23865 603 41 0 29168 0 vsize: 116836 [startup+540.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24541 0 0 0 53952 58 0 0 25 0 1 0 546185186 119640064 23870 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29209 23870 603 41 0 29168 0 vsize: 116836 [startup+550.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24546 0 0 0 54952 58 0 0 25 0 1 0 546185186 119640064 23875 4294967295 134512640 134672761 3221224544 3221223392 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29209 23875 603 41 0 29168 0 vsize: 116836 [startup+560.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24548 0 0 0 55952 58 0 0 25 0 1 0 546185186 119640064 23877 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29209 23877 603 41 0 29168 0 vsize: 116836 [startup+570.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24548 0 0 0 56952 58 0 0 25 0 1 0 546185186 119640064 23877 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29209 23877 603 41 0 29168 0 vsize: 116836 [startup+580.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24548 0 0 0 57952 58 0 0 25 0 1 0 546185186 119640064 23877 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29209 23877 603 41 0 29168 0 vsize: 116836 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24557 0 0 0 58952 58 0 0 25 0 1 0 546185186 119771136 23886 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29241 23886 603 41 0 29200 0 vsize: 116964 [startup+600.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24573 0 0 0 59952 58 0 0 25 0 1 0 546185186 119771136 23902 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29241 23902 603 41 0 29200 0 vsize: 116964 [startup+610.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24589 0 0 0 60953 58 0 0 25 0 1 0 546185186 119771136 23918 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29241 23918 603 41 0 29200 0 vsize: 116964 [startup+620.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24601 0 0 0 61953 58 0 0 25 0 1 0 546185186 119910400 23930 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29275 23930 603 41 0 29234 0 vsize: 117100 [startup+630.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24615 0 0 0 62953 58 0 0 25 0 1 0 546185186 119910400 23944 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29275 23944 603 41 0 29234 0 vsize: 117100 [startup+640.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24621 0 0 0 63953 58 0 0 25 0 1 0 546185186 119910400 23950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29275 23950 603 41 0 29234 0 vsize: 117100 [startup+650.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24632 0 0 0 64953 58 0 0 25 0 1 0 546185186 120045568 23961 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29308 23961 603 41 0 29267 0 vsize: 117232 [startup+660.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24640 0 0 0 65953 58 0 0 25 0 1 0 546185186 120045568 23969 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29308 23969 603 41 0 29267 0 vsize: 117232 [startup+670.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24650 0 0 0 66953 58 0 0 25 0 1 0 546185186 120045568 23979 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29308 23979 603 41 0 29267 0 vsize: 117232 [startup+680.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24660 0 0 0 67954 58 0 0 25 0 1 0 546185186 120168448 23989 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29338 23989 603 41 0 29297 0 vsize: 117352 [startup+690.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24667 0 0 0 68954 58 0 0 25 0 1 0 546185186 120168448 23996 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29338 23996 603 41 0 29297 0 vsize: 117352 [startup+700.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 902 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24705 0 0 0 69954 58 0 0 25 0 1 0 546185186 120279040 24034 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29365 24034 603 41 0 29324 0 vsize: 117460 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24718 0 0 0 70954 58 0 0 25 0 1 0 546185186 120279040 24047 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29365 24047 603 41 0 29324 0 vsize: 117460 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24718 0 0 0 71954 58 0 0 25 0 1 0 546185186 120279040 24047 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29365 24047 603 41 0 29324 0 vsize: 117460 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24722 0 0 0 72955 58 0 0 25 0 1 0 546185186 120406016 24051 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29396 24051 603 41 0 29355 0 vsize: 117584 [startup+740.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24731 0 0 0 73955 58 0 0 25 0 1 0 546185186 120406016 24060 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29396 24060 603 41 0 29355 0 vsize: 117584 [startup+750.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24746 0 0 0 74955 58 0 0 25 0 1 0 546185186 120406016 24075 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29396 24075 603 41 0 29355 0 vsize: 117584 [startup+760.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24761 0 0 0 75955 59 0 0 25 0 1 0 546185186 120532992 24090 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29427 24090 603 41 0 29386 0 vsize: 117708 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24769 0 0 0 76955 59 0 0 25 0 1 0 546185186 120532992 24098 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29427 24098 603 41 0 29386 0 vsize: 117708 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24776 0 0 0 77955 59 0 0 25 0 1 0 546185186 120532992 24105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29427 24105 603 41 0 29386 0 vsize: 117708 [startup+790.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24790 0 0 0 78955 59 0 0 25 0 1 0 546185186 120664064 24119 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29459 24119 603 41 0 29418 0 vsize: 117836 [startup+800.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24796 0 0 0 79955 59 0 0 25 0 1 0 546185186 120664064 24125 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29459 24125 603 41 0 29418 0 vsize: 117836 [startup+810.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24816 0 0 0 80955 59 0 0 25 0 1 0 546185186 120786944 24145 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29489 24145 603 41 0 29448 0 vsize: 117956 [startup+820.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24829 0 0 0 81955 59 0 0 25 0 1 0 546185186 120786944 24158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29489 24158 603 41 0 29448 0 vsize: 117956 [startup+830.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24843 0 0 0 82956 59 0 0 25 0 1 0 546185186 120786944 24172 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29489 24172 603 41 0 29448 0 vsize: 117956 [startup+840.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24852 0 0 0 83956 59 0 0 25 0 1 0 546185186 120918016 24181 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29521 24181 603 41 0 29480 0 vsize: 118084 [startup+850.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24866 0 0 0 84956 59 0 0 25 0 1 0 546185186 120918016 24195 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29521 24195 603 41 0 29480 0 vsize: 118084 [startup+860.164 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24877 0 0 0 85966 59 0 0 25 0 1 0 546185186 121044992 24206 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29552 24206 603 41 0 29511 0 vsize: 118208 [startup+870.163 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24880 0 0 0 86966 59 0 0 25 0 1 0 546185186 121044992 24209 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29552 24209 603 41 0 29511 0 vsize: 118208 [startup+880.164 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24894 0 0 0 87967 59 0 0 25 0 1 0 546185186 121044992 24223 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29552 24223 603 41 0 29511 0 vsize: 118208 [startup+890.165 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24903 0 0 0 88967 59 0 0 25 0 1 0 546185186 121044992 24232 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29552 24232 603 41 0 29511 0 vsize: 118208 [startup+900.164 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24938 0 0 0 89967 60 0 0 25 0 1 0 546185186 121171968 24267 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29583 24267 603 41 0 29542 0 vsize: 118332 [startup+910.165 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24938 0 0 0 90967 60 0 0 25 0 1 0 546185186 121171968 24267 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29583 24267 603 41 0 29542 0 vsize: 118332 [startup+920.166 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24944 0 0 0 91967 60 0 0 25 0 1 0 546185186 121307136 24273 4294967295 134512640 134672761 3221224544 3221223808 134562494 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29616 24273 603 41 0 29575 0 vsize: 118464 [startup+930.167 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24951 0 0 0 92967 60 0 0 25 0 1 0 546185186 121307136 24280 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29616 24280 603 41 0 29575 0 vsize: 118464 [startup+940.174 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24959 0 0 0 93968 60 0 0 25 0 1 0 546185186 121307136 24288 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29616 24288 603 41 0 29575 0 vsize: 118464 [startup+950.184 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24974 0 0 0 94969 60 0 0 25 0 1 0 546185186 121438208 24303 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29648 24303 603 41 0 29607 0 vsize: 118592 [startup+960.185 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 24988 0 0 0 95970 60 0 0 25 0 1 0 546185186 121438208 24317 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29648 24317 603 41 0 29607 0 vsize: 118592 [startup+970.185 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25013 0 0 0 96970 60 0 0 25 0 1 0 546185186 121565184 24342 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29679 24342 603 41 0 29638 0 vsize: 118716 [startup+980.186 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25034 0 0 0 97970 60 0 0 25 0 1 0 546185186 121565184 24363 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29679 24363 603 41 0 29638 0 vsize: 118716 [startup+990.185 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25047 0 0 0 98970 60 0 0 25 0 1 0 546185186 121696256 24376 4294967295 134512640 134672761 3221224544 3221223600 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29711 24376 603 41 0 29670 0 vsize: 118844 [startup+1000.2 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 904 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25058 0 0 0 99971 60 0 0 25 0 1 0 546185186 121696256 24387 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29711 24387 603 41 0 29670 0 vsize: 118844 [startup+1010.2 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25072 0 0 0 100972 60 0 0 25 0 1 0 546185186 121819136 24401 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29741 24401 603 41 0 29700 0 vsize: 118964 [startup+1020.2 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25082 0 0 0 101972 60 0 0 25 0 1 0 546185186 121819136 24411 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29741 24411 603 41 0 29700 0 vsize: 118964 [startup+1030.21 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25093 0 0 0 102972 60 0 0 25 0 1 0 546185186 121819136 24422 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29741 24422 603 41 0 29700 0 vsize: 118964 [startup+1040.21 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25105 0 0 0 103972 60 0 0 25 0 1 0 546185186 121950208 24434 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29773 24434 603 41 0 29732 0 vsize: 119092 [startup+1050.21 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25117 0 0 0 104972 60 0 0 25 0 1 0 546185186 121950208 24446 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29773 24446 603 41 0 29732 0 vsize: 119092 [startup+1060.21 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25126 0 0 0 105973 60 0 0 25 0 1 0 546185186 121950208 24455 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29773 24455 603 41 0 29732 0 vsize: 119092 [startup+1070.23 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25145 0 0 0 106975 60 0 0 25 0 1 0 546185186 122085376 24474 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29806 24474 603 41 0 29765 0 vsize: 119224 [startup+1080.24 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25159 0 0 0 107977 60 0 0 25 0 1 0 546185186 122085376 24488 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29806 24488 603 41 0 29765 0 vsize: 119224 [startup+1090.26 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25173 0 0 0 108979 61 0 0 25 0 1 0 546185186 122220544 24502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29839 24502 603 41 0 29798 0 vsize: 119356 [startup+1100.26 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25187 0 0 0 109978 61 0 0 25 0 1 0 546185186 122220544 24516 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29839 24516 603 41 0 29798 0 vsize: 119356 [startup+1110.37 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25197 0 0 0 110989 61 0 0 25 0 1 0 546185186 122351616 24526 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29871 24526 603 41 0 29830 0 vsize: 119484 [startup+1120.37 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25211 0 0 0 111989 61 0 0 25 0 1 0 546185186 122351616 24540 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29871 24540 603 41 0 29830 0 vsize: 119484 [startup+1130.39 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25222 0 0 0 112991 61 0 0 25 0 1 0 546185186 122351616 24551 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29871 24551 603 41 0 29830 0 vsize: 119484 [startup+1140.39 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25234 0 0 0 113991 61 0 0 25 0 1 0 546185186 122486784 24563 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29904 24563 603 41 0 29863 0 vsize: 119616 [startup+1150.39 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25241 0 0 0 114992 61 0 0 25 0 1 0 546185186 122486784 24570 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29904 24570 603 41 0 29863 0 vsize: 119616 [startup+1160.4 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25259 0 0 0 115993 61 0 0 25 0 1 0 546185186 122613760 24588 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29935 24588 603 41 0 29894 0 vsize: 119740 [startup+1170.5 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25276 0 0 0 117003 61 0 0 25 0 1 0 546185186 122613760 24605 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29935 24605 603 41 0 29894 0 vsize: 119740 [startup+1180.51 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25282 0 0 0 118004 61 0 0 25 0 1 0 546185186 122613760 24611 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29935 24611 603 41 0 29894 0 vsize: 119740 [startup+1190.54 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25293 0 0 0 119007 61 0 0 25 0 1 0 546185186 122740736 24622 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29966 24622 603 41 0 29925 0 vsize: 119864 [startup+1200.57 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 906 Raw data (stat): 898 (minisat+) R 897 20024 20023 0 -1 0 25307 0 0 0 120010 61 0 0 25 0 1 0 546185186 122740736 24636 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29966 24636 603 41 0 29925 0 vsize: 119864 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1201.02 s] Raw data (loadavg): 0.99 0.97 0.91 1/55 906 Raw data (stat): 898 (minisat+) Z 897 20024 20023 0 -1 12 25310 0 0 0 120010 66 0 0 20 0 1 0 546185186 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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): 1201.02 CPU time (s): 1200.77 CPU user time (s): 1200.11 CPU system time (s): 0.665898 CPU usage (%): 99.9795 Max. virtual memory (Kb): 119864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####