WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:            90                                         |
|  Number of clauses:             415                                         |
|  Parse time:                   0.00 s                                       |
|                                                                             |
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
|       100 |      90      415      900 |      152      100     24 |  0.012 % |
|       250 |      90      415      900 |      167      149     24 |  0.012 % |
|       475 |      90      415      900 |      184      167     26 |  0.012 % |
|       812 |      90      415      900 |      202      101     20 |  0.012 % |
|      1318 |      90      415      900 |      222      121     23 |  0.012 % |
|      2077 |      90      415      900 |      245      249     28 |  0.012 % |
|      3216 |      90      415      900 |      269      185     22 |  0.012 % |
|      4924 |      90      415      900 |      296      181     22 |  0.012 % |
|      7486 |      90      415      900 |      326      184     22 |  0.012 % |
|     11330 |      90      415      900 |      358      357     29 |  0.012 % |
|     17096 |      90      415      900 |      394      268     26 |  0.012 % |
|     25745 |      90      415      900 |      434      398     28 |  0.012 % |
|     38719 |      90      415      900 |      477      255     24 |  0.012 % |
|     58180 |      90      415      900 |      525      420     27 |  0.012 % |
|     87372 |      90      415      900 |      577      499     27 |  0.012 % |
|    131161 |      90      415      900 |      635      373     28 |  0.012 % |
|    196845 |      90      415      900 |      699      410     25 |  0.012 % |
===============================================================================
restarts              : 638
conflicts             : 274072         (172449 /sec)
decisions             : 336451         (0.00 % random) (211699 /sec)
propagations          : 3674326        (2311931 /sec)
conflict literals     : 7499516        (9.26 % deleted)
Memory used           : 10.00 MB
CPU time              : 1.58929 s

UNSATISFIABLE