c
c This is glucose 4.0 --  based on MiniSAT (Many thanks to MiniSAT team)
c
c ========================================[ Problem Statistics ]===========================================
c |                                                                                                       |
c |  Number of variables:     106133312                                                                   |
c |  Number of clauses:        98916961                                                                   |
c |  Parse time:                 708.41 s                                                                 |
c |                                                                                                       |
c | Preprocesing is fully done
c |  Simplification time:          0.00 s                                                                 |
c |                                                                                                       |
c =========================================================================================================
Solved by simplification
c restarts              : 0 (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             : 0              (-nan % random) (0 /sec)
c propagations          : 47848660       (67544 /sec)
c conflict literals     : 0              (-nan % deleted)
c nb reduced Clauses    : 0
c CPU time              : 708.408 s

s UNSATISFIABLE