c ============================[ Problem Statistics ]=============================
c |                                                                             |
c |  Number of variables:           589                                         |
c |  Number of clauses:            1422                                         |
c |  Parse time:                   0.00 s                                       |
c |                                                                             |
c ============================[ Search Statistics ]==============================
c | Conflicts |          ORIGINAL         |          LEARNT          | Progress |
c |           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
c ===============================================================================
c |       100 |     589     1422     3800 |      521      100     32 |  0.003 % |
c |       250 |     589     1422     3800 |      573      250     33 |  0.001 % |
c |       475 |     589     1422     3800 |      630      475     31 |  0.000 % |
c |       812 |     589     1422     3800 |      693      408     25 |  0.000 % |
c |      1318 |     589     1422     3800 |      763      511     27 |  0.000 % |
c |      2077 |     589     1422     3800 |      839      466     26 |  0.000 % |
c |      3216 |     589     1422     3800 |      923      629     29 |  0.002 % |
c |      4924 |     589     1422     3800 |     1016      887     34 |  0.000 % |
c |      7486 |     589     1422     3800 |     1117      759     31 |  0.000 % |
c |     11330 |     589     1422     3800 |     1229      935     29 |  0.000 % |
c |     17096 |     589     1422     3800 |     1352      733     28 |  0.000 % |
c |     25745 |     589     1422     3800 |     1487      762     29 |  0.000 % |
c |     38719 |     589     1422     3800 |     1636     1171     29 |  0.000 % |
c |     58180 |     589     1422     3800 |     1800     1645     35 |  0.000 % |
c |     87372 |     589     1422     3800 |     1980     1538     32 |  0.000 % |
c |    131161 |     589     1422     3800 |     2178     1772     31 |  0.000 % |
c |    196845 |     589     1422     3800 |     2395     1547     29 |  0.002 % |
c |    295371 |     589     1422     3800 |     2635     1296     30 |  0.000 % |
c ===============================================================================
c restarts              : 766
c conflicts             : 325046      
c decisions             : 408927         (0.00 % random)
c propagations          : 17191748    
c conflict literals     : 12453793       (12.79 % deleted)
c CPU time              : 10.002s
s INDETERMINATE