WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:            72                                         |
|  Number of clauses:             297                                         |
|  Parse time:                   0.00 s                                       |
|                                                                             |
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
|       100 |      72      297      648 |      108      100     19 |  0.020 % |
|       250 |      72      297      648 |      119      111     18 |  0.020 % |
|       475 |      72      297      648 |      131       91     16 |  0.020 % |
|       812 |      72      297      648 |      144      116     18 |  0.020 % |
|      1318 |      72      297      648 |      159      101     18 |  0.174 % |
|      2077 |      72      297      648 |      175      170     20 |  0.020 % |
|      3216 |      72      297      648 |      192      123     17 |  0.020 % |
|      4924 |      72      297      648 |      212      183     21 |  0.020 % |
|      7486 |      72      297      648 |      233      205     22 |  0.020 % |
|     11330 |      72      297      648 |      256      254     21 |  0.020 % |
|     17096 |      72      297      648 |      282      216     20 |  0.020 % |
|     25745 |      72      297      648 |      310      212     19 |  0.020 % |
|     38719 |      72      297      648 |      341      291     18 |  0.020 % |
===============================================================================
restarts              : 127
conflicts             : 41414          (230357 /sec)
decisions             : 51044          (0.00 % random) (283922 /sec)
propagations          : 515393         (2866766 /sec)
conflict literals     : 898230         (9.52 % deleted)
Memory used           : 10.00 MB
CPU time              : 0.179782 s

UNSATISFIABLE