c launch: /data/cnf/sc2014/app/esawn_uw3.debugged.cnf.bz2
c host: atom17
c [bunzip2-and-then] start copying and unzipping '/data/cnf/sc2014/app/esawn_uw3.debugged.cnf.bz2' at Thu May  7 15:37:44 CEST 2015
c [bunzip2-and-then] unzipped into '/tmp/bunzip2-and-then-unzipped' at Thu May  7 15:38:24 CEST 2015
c
c This is glucose 2.3 --  based on MiniSAT (Many thanks to MiniSAT team)
c Simplification mode is turned on
c
c ========================================[ Problem Statistics ]===========================================
c |                                                                                                       |
c |  Number of variables:      13842706                                                                   |
c |  Number of clauses:        51484923                                                                   |
c |  Parse time:                  25.93 s                                                                 |
c |                                                                                                       |
c Too many clauses... No preprocessing
c |  Simplification time:          5.19 s                                                                 |
c |                                                                                                       |
c ========================================[ MAGIC CONSTANTS ]==============================================
c | Constants are supposed to work well together :-)                                                      |
c | however, if you find better choices, please let us known...                                           |
c |-------------------------------------------------------------------------------------------------------|
c |                                |                                |                                     |
c | - Restarts:                    | - Reduce Clause DB:            | - Minimize Asserting:               |
c |   * LBD Queue    :     50      |   * First     :   2000         |    * size <  30                     |
c |   * Trail  Queue :   5000      |   * Inc       :    300         |    * lbd  <   6                     |
c |   * K            :   0.80      |   * Special   :   1000         |                                     |
c |   * R            :   1.40      |   * Protected :  (lbd)< 30     |                                     |
c |                                |                                |                                     |
c ==================================[ Search Statistics (every  10000 conflicts) ]=========================
c |                                                                                                       |
c |          RESTARTS           |          ORIGINAL         |              LEARNT              | Progress |
c |       NB   Blocked  Avg Cfc |    Vars  Clauses Literals |   Red   Learnts    LBD2  Removed |          |
c =========================================================================================================
c last restart ## conflicts  :  364 69815 
c =========================================================================================================
c restarts              : 25 (191 conflicts in avg)
c blocked restarts      : 0 (multiple: 0) 
c last block at restart : 0
c nb ReduceDB           : 0
c nb removed Clauses    : 0
c nb learnts DL2        : 893
c nb learnts size 2     : 381
c nb learnts size 1     : 17
c conflicts             : 4783           (16 /sec)
c decisions             : 18445794       (0.00 % random) (59830 /sec)
c propagations          : 975097385      (3162792 /sec)
c conflict literals     : 42963          (34.25 % deleted)
c nb reduced Clauses    : 182
c Memory used           : 7261.00 MB
c CPU time              : 308.303 s

s SATISFIABLE
c launch: done
