gistfile1.txt

============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:         13408                                         |
|  Number of clauses:            8320                                         |
|  Parse time:                   0.02 s                                       |
|  Simplification time:          0.00 s                                       |
|                                                                             |
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
|       100 |   12868     7680    23040 |     2816      100     27 |  2.200 % |
|       250 |   12868     7680    23040 |     3097      250     34 |  2.200 % |
|       475 |   12868     7680    23040 |     3407      475     45 |  2.200 % |
|       812 |   12868     7680    23040 |     3748      812     49 |  2.200 % |
|      1318 |   12868     7680    23040 |     4122     1318     96 |  2.200 % |
|      2077 |   12868     7680    23040 |     4535     2077     95 |  2.200 % |
|      3216 |   12868     7680    23040 |     4988     3216    157 |  2.200 % |
|      4924 |   12868     7680    23040 |     5487     4924    123 |  2.200 % |
|      7486 |   12868     7680    23040 |     6036     4278     52 |  2.200 % |
|     11330 |   12868     7680    23040 |     6639     4915     81 |  2.200 % |
|     17096 |   12868     7680    23040 |     7303     7068    246 |  2.200 % |
|     25745 |   12868     7680    23040 |     8034     7191    139 |  2.200 % |
|     38719 |   12868     7680    23040 |     8837     5913    238 |  2.200 % |
|     58180 |   12868     7680    23040 |     9721     5406    155 |  2.200 % |
|     87372 |   12868     7680    23040 |    10693    13805    310 |  2.200 % |
|    131161 |   12868     7680    23040 |    11763     7084    204 |  2.200 % |
|    196845 |   12868     7680    23040 |    12939    13102    321 |  2.200 % |
|    295371 |   12868     7680    23040 |    14233     7861    103 |  2.200 % |
|    443160 |   12868     7680    23040 |    15656     9655    185 |  2.200 % |
|    664843 |   12868     7680    23040 |    17222    12612    162 |  2.200 % |
|    997368 |   12868     7680    23040 |    18944    14851    504 |  2.200 % |
|   1496156 |   12868     7680    23040 |    20839    16638    266 |  2.200 % |
|   2244338 |   12868     7680    23040 |    22923    13123    270 |  2.200 % |
|   3366612 |   12868     7680    23040 |    25215    20013    158 |  2.200 % |
|   5050023 |   12868     7680    23040 |    27736    14840    396 |  2.200 % |
|   7575139 |   12868     7680    23040 |    30510    29314   1069 |  2.200 % |
|  11362814 |   12868     7680    23040 |    33561    29701    695 |  2.200 % |
|  17044326 |   12868     7680    23040 |    36917    33667    485 |  2.200 % |
|  25566595 |   12868     7680    23040 |    40609    15928     57 |  2.200 % |
|  38349998 |   12868     7680    23040 |    44670    34741    242 |  2.200 % |
|  57525103 |   12868     7680    23040 |    49137    44063    375 |  2.200 % |
|  86287761 |   12868     7680    23040 |    54051    18355     45 |  2.200 % |
| 129431749 |   12868     7680    23040 |    59456    44745    263 |  2.200 % |
| 194147731 |   12868     7680    23040 |    65402    21474    153 |  2.200 % |
| 291221704 |   12868     7680    23040 |    71942    47665    202 |  2.200 % |
| 436832664 |   12868     7680    23040 |    79136    45468     82 |  2.200 % |
| 655249104 |   12868     7680    23040 |    87050    65493    121 |  2.200 % |
| 982873765 |   12868     7680    23040 |    95755    49251    214 |  2.200 % |
| 1474310757 |   12868     7680    23040 |   105330    33816    197 |  2.200 % |