c launch: /data/cnf/sc2014/app/complete-300-0.1-18-98765432130018.cnf.bz2
c host: atom25
c [bunzip2-and-then] start copying and unzipping '/data/cnf/sc2014/app/complete-300-0.1-18-98765432130018.cnf.bz2' at Thu May  7 14:08:40 CEST 2015
c [bunzip2-and-then] unzipped into '/tmp/bunzip2-and-then-unzipped' at Thu May  7 14:08:40 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:           600                                                                   |
c |  Number of clauses:           27034                                                                   |
c |  Parse time:                   0.04 s                                                                 |
c |                                                                                                       |
c |  Simplification time:          0.67 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  :  0 8 
c =========================================================================================================
c restarts              : 1 (0 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        : 0
c nb learnts size 2     : 0
c nb learnts size 1     : 0
c conflicts             : 0              (0 /sec)
c decisions             : 9              (0.00 % random) (13 /sec)
c propagations          : 600            (845 /sec)
c conflict literals     : 0              (-nan % deleted)
c nb reduced Clauses    : 0
c Memory used           : 11.00 MB
c CPU time              : 0.70983 s

s SATISFIABLE
c launch: done
