c
c This is glucose-syrup 4.0 (glucose in many threads) --  based on MiniSAT (Many thanks to MiniSAT team)
c
c WARNING: for repeatability, setting FPU to use double precision
c 2 solvers engines and 1 companion as a blackboard created.
c ========================================[ Problem Statistics ]===========================================
c |                                                                                                       |
c |  Number of variables:        892948                                                                   |
c |  Number of clauses:         1928884                                                                   |
c |  Parse time:                   0.42 s                                                                 |
c |                                                                                                       |
c |  Eliminated clauses:           0.14 Mb                                                                |
c |  Simplification time:          0.56 s                                                                 |
c |                                                                                                       |
c |  Generating clones                                                                                    |
c |  all clones generated. Memory = 498.76Mb.                                                             |
c ========================================================================================================|
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |      1 |      91236 |       1678 |     8140 |     1677 |        0 |        0 |        0 | 25.644 |
c |  1 |      4 |      67150 |       1160 |    10596 |     1160 |        0 |        0 |        0 | 25.644 |
c 
c synthesis        2838 conflicts    66435237 propagations      293 conflicts/sec  6853876 propagations/sec
c Total Memory so far : 642.77Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |      1 |      94427 |       3379 |    11643 |     2384 |        0 |        0 |        0 | 25.644 |
c |  1 |      4 |      70610 |       2499 |    22123 |     1505 |        0 |        0 |        0 | 25.644 |
c 
c synthesis        5878 conflicts   137251210 propagations      300 conflicts/sec  6994625 propagations/sec
c Total Memory so far : 642.77Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |      5 |     100802 |       4885 |    21742 |     2096 |        0 |        0 |        0 | 25.644 |
c |  1 |      8 |      74608 |       3608 |    33085 |     2615 |        0 |        0 |        0 | 25.644 |
c 
c synthesis        8493 conflicts   211041133 propagations      288 conflicts/sec  7145216 propagations/sec
c Total Memory so far : 642.89Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |      5 |     102826 |       5854 |    27331 |     3066 |      292 |        0 |        0 | 25.644 |
c |  1 |     11 |      77884 |       4606 |    43248 |     3613 |        0 |      211 |        1 | 25.644 |
c 
c synthesis       10460 conflicts   270282723 propagations      279 conflicts/sec  7210337 propagations/sec
c Total Memory so far : 642.89Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     14 |     109527 |       6838 |    35114 |     4050 |      477 |      255 |        0 | 25.644 |
c |  1 |     11 |      79723 |       5519 |    48814 |     4526 |      265 |      211 |        2 | 25.644 |
c 
c synthesis       12357 conflicts   332726973 propagations      272 conflicts/sec  7324156 propagations/sec
c Total Memory so far : 642.89Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     15 |     112286 |       7952 |    42788 |     2663 |      781 |      270 |        2 | 25.644 |
c |  1 |     12 |      82141 |       6469 |    55630 |     5476 |      605 |      711 |        3 | 25.644 |
c 
c synthesis       14421 conflicts   392159582 propagations      270 conflicts/sec  7347345 propagations/sec
c Total Memory so far : 643.02Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     15 |     114300 |       8983 |    48155 |     3695 |     1056 |      270 |        2 | 25.644 |
c |  1 |     12 |      84406 |       7603 |    61012 |     3816 |      824 |      711 |        4 | 25.644 |
c 
c synthesis       16586 conflicts   447102928 propagations      270 conflicts/sec  7291107 propagations/sec
c Total Memory so far : 643.02Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     18 |     119250 |      10020 |    58105 |     4732 |     1300 |      973 |        5 | 25.644 |
c |  1 |     13 |      87277 |       8724 |    66199 |     4937 |     1026 |     1252 |        5 | 25.644 |
c 
c synthesis       18744 conflicts   506091840 propagations      271 conflicts/sec  7306024 propagations/sec
c Total Memory so far : 643.02Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     21 |     122479 |      11122 |    65827 |     5834 |     1509 |     1074 |       10 | 25.644 |
c |  1 |     17 |      91887 |       9764 |    74140 |     5977 |     1289 |     1473 |       10 | 25.644 |
c 
c synthesis       20886 conflicts   563839922 propagations      270 conflicts/sec  7302149 propagations/sec
c Total Memory so far : 643.02Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     21 |     124331 |      12183 |    71309 |     6895 |     1697 |     1074 |       13 | 25.644 |
c |  1 |     18 |      94955 |      10755 |    81488 |     6968 |     1522 |     1571 |       14 | 25.644 |
c 
c synthesis       22938 conflicts   618735031 propagations      269 conflicts/sec  7265427 propagations/sec
c Total Memory so far : 643.15Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     24 |     127388 |      13217 |    76780 |     7928 |     1907 |     1670 |       18 | 25.644 |
c |  1 |     21 |      98527 |      11727 |    86813 |     7939 |     1759 |     1825 |       17 | 25.644 |
c 
c synthesis       24944 conflicts   674750365 propagations      268 conflicts/sec  7247081 propagations/sec
c Total Memory so far : 643.15Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     24 |     129718 |      14379 |    82232 |     9090 |     2188 |     1670 |       18 | 25.644 |
c |  1 |     23 |     101738 |      12743 |    91092 |     8956 |     2026 |     2179 |       17 | 25.644 |
c 
c synthesis       27122 conflicts   734887800 propagations      268 conflicts/sec  7272298 propagations/sec
c Total Memory so far : 643.15Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     27 |     132629 |      15358 |    88995 |    10070 |     2386 |     2179 |       22 | 25.644 |
c |  1 |     28 |     106971 |      13673 |    97877 |     9885 |     2199 |     2321 |       22 | 25.644 |
c 
c synthesis       29031 conflicts   796088661 propagations      266 conflicts/sec  7303498 propagations/sec
c Total Memory so far : 643.28Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     34 |     138126 |      16363 |    96737 |     5922 |     2555 |     2404 |       32 | 25.644 |
c |  1 |     28 |     108942 |      14662 |   103085 |     5873 |     2406 |     2321 |       28 | 25.644 |
c 
c synthesis       31025 conflicts   851098207 propagations      265 conflicts/sec  7279482 propagations/sec
c Total Memory so far : 643.28Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     37 |     143484 |      17370 |   104414 |     6930 |     2773 |     2521 |       36 | 25.644 |
c |  1 |     28 |     110794 |      15615 |   107089 |     6826 |     2629 |     2321 |       30 | 25.644 |
c 
c synthesis       32985 conflicts   911392757 propagations      264 conflicts/sec  7298991 propagations/sec
c Total Memory so far : 643.28Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     47 |     149406 |      18348 |   110717 |     7908 |     2927 |     2854 |       44 | 25.644 |
c |  1 |     28 |     112237 |      16581 |   109743 |     7792 |     2858 |     2321 |       35 | 25.644 |
c 
c synthesis       34929 conflicts   972019645 propagations      263 conflicts/sec  7318684 propagations/sec
c Total Memory so far : 643.28Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     50 |     153090 |      19398 |   116820 |     8958 |     3128 |     3059 |       51 | 25.644 |
c |  1 |     28 |     113646 |      17511 |   111901 |     8722 |     3066 |     2321 |       36 | 25.644 |
c 
c synthesis       36909 conflicts  1031622845 propagations      262 conflicts/sec  7328940 propagations/sec
c Total Memory so far : 643.41Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     57 |     159178 |      20326 |   124084 |     9886 |     3308 |     3215 |       64 | 25.644 |
c |  1 |     28 |     115266 |      18445 |   114492 |     9656 |     3224 |     2321 |       41 | 25.644 |
c 
c synthesis       38771 conflicts  1091230193 propagations      261 conflicts/sec  7337978 propagations/sec
c Total Memory so far : 643.41Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     63 |     164618 |      21402 |   130920 |    10962 |     3485 |     3325 |       72 | 25.644 |
c |  1 |     28 |     116659 |      19290 |   116503 |    10501 |     3412 |     2321 |       41 | 25.644 |
c 
c synthesis       40692 conflicts  1149108197 propagations      260 conflicts/sec  7335006 propagations/sec
c Total Memory so far : 643.41Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     68 |     169265 |      22436 |   137246 |    11996 |     3680 |     3532 |       80 | 25.644 |
c |  1 |     28 |     118122 |      20119 |   118451 |    11330 |     3623 |     2321 |       43 | 25.644 |
c 
c synthesis       42555 conflicts  1205679635 propagations      259 conflicts/sec  7324566 propagations/sec
c Total Memory so far : 643.41Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     73 |     172986 |      23473 |   142527 |    13033 |     3797 |     3763 |       91 | 25.644 |
c |  1 |     28 |     119519 |      20977 |   120798 |    12188 |     3763 |     2321 |       45 | 25.644 |
c 
c synthesis       44450 conflicts  1264983609 propagations      258 conflicts/sec  7330868 propagations/sec
c Total Memory so far : 643.54Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     77 |     176908 |      24433 |   149311 |    13993 |     3797 |     3763 |       99 | 25.644 |
c |  1 |     28 |     120870 |      21848 |   123044 |    13059 |     3763 |     2321 |       48 | 25.644 |
c 
c synthesis       46281 conflicts  1324346905 propagations      256 conflicts/sec  7336812 propagations/sec
c Total Memory so far : 643.54Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     81 |     180794 |      25417 |   155017 |    14977 |     3797 |     3763 |      104 | 25.644 |
c |  1 |     28 |     122473 |      22713 |   126487 |    13924 |     3763 |     2321 |       51 | 25.644 |
c 
c synthesis       48130 conflicts  1382022782 propagations      255 conflicts/sec  7333344 propagations/sec
c Total Memory so far : 643.54Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     81 |     182992 |      26387 |   159066 |     8177 |     3797 |     3763 |      118 | 25.644 |
c |  1 |     28 |     123916 |      23549 |   129674 |    14759 |     3763 |     2321 |       55 | 25.644 |
c 
c synthesis       49936 conflicts  1440288644 propagations      254 conflicts/sec  7333176 propagations/sec
c Total Memory so far : 643.68Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     83 |     185847 |      27412 |   164002 |     9201 |     3797 |     3763 |      126 | 25.644 |
c |  1 |     28 |     125423 |      24469 |   131680 |     8278 |     3763 |     2321 |       60 | 25.644 |
c 
c synthesis       51881 conflicts  1500618163 propagations      254 conflicts/sec  7343066 propagations/sec
c Total Memory so far : 643.68Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     84 |     188240 |      28551 |   166442 |    10341 |     3797 |     3763 |      130 | 25.644 |
c |  1 |     28 |     126993 |      25417 |   133710 |     9226 |     3763 |     2321 |       63 | 25.644 |
c 
c synthesis       53968 conflicts  1560166254 propagations      254 conflicts/sec  7348600 propagations/sec
c Total Memory so far : 643.68Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     89 |     191422 |      29520 |   170950 |    11310 |     3797 |     3763 |      143 | 25.644 |
c |  1 |     28 |     128831 |      26363 |   136166 |    10171 |     3763 |     2321 |       69 | 25.644 |
c 
c synthesis       55883 conflicts  1617691730 propagations      254 conflicts/sec  7344648 propagations/sec
c Total Memory so far : 673.78Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     97 |     197876 |      30555 |   176636 |    12345 |     3797 |     3763 |      148 | 25.644 |
c |  1 |     28 |     130224 |      27244 |   138686 |    11053 |     3763 |     2321 |       71 | 25.644 |
c 
c synthesis       57799 conflicts  1675035750 propagations      253 conflicts/sec  7340130 propagations/sec
c Total Memory so far : 673.78Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     97 |     199454 |      31605 |   180582 |    13394 |     3797 |     3763 |      151 | 25.644 |
c |  1 |     28 |     131700 |      28118 |   140757 |    11927 |     3763 |     2321 |       71 | 25.644 |
c 
c synthesis       59723 conflicts  1731989710 propagations      253 conflicts/sec  7334287 propagations/sec
c Total Memory so far : 673.78Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |     97 |     200993 |      32449 |   185643 |    14239 |     3797 |     3763 |      158 | 25.644 |
c |  1 |     28 |     133305 |      29045 |   142505 |    12854 |     3763 |     2321 |       71 | 25.644 |
c 
c synthesis       61494 conflicts  1788341189 propagations      252 conflicts/sec  7326309 propagations/sec
c Total Memory so far : 673.78Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    101 |     203990 |      33412 |   189286 |    15202 |     3797 |     3763 |      166 | 25.644 |
c |  1 |     28 |     134640 |      29863 |   144485 |    13672 |     3763 |     2321 |       73 | 25.644 |
c 
c synthesis       63275 conflicts  1844080255 propagations      251 conflicts/sec  7316408 propagations/sec
c Total Memory so far : 673.91Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    101 |     206111 |      34503 |   191528 |    16292 |     3797 |     3763 |      169 | 25.644 |
c |  1 |     28 |     136058 |      30717 |   146447 |    14526 |     3763 |     2321 |       75 | 25.644 |
c 
c synthesis       65220 conflicts  1902448696 propagations      251 conflicts/sec  7317197 propagations/sec
c Total Memory so far : 673.91Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    101 |     208197 |      35638 |   192851 |    17428 |     3797 |     3763 |      170 | 25.644 |
c |  1 |     28 |     137368 |      31625 |   147964 |    15434 |     3763 |     2321 |       75 | 25.644 |
c 
c synthesis       67263 conflicts  1958669965 propagations      251 conflicts/sec  7309972 propagations/sec
c Total Memory so far : 673.91Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    105 |     212701 |      36692 |   196736 |    18482 |     3797 |     3763 |      177 | 25.644 |
c |  1 |     28 |     139064 |      32557 |   149714 |    16366 |     3763 |     2321 |       77 | 25.644 |
c 
c synthesis       69249 conflicts  2015921802 propagations      251 conflicts/sec  7306880 propagations/sec
c Total Memory so far : 704.00Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    107 |     215654 |      37817 |   198240 |    19607 |     3797 |     3763 |      179 | 25.644 |
c |  1 |     28 |     140625 |      33532 |   151126 |    17341 |     3763 |     2321 |       82 | 25.644 |
c 
c synthesis       71349 conflicts  2072130142 propagations      251 conflicts/sec  7300276 propagations/sec
c Total Memory so far : 704.13Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    112 |     220256 |      38789 |   203583 |    20579 |     3797 |     3763 |      197 | 25.644 |
c |  1 |     28 |     142047 |      34450 |   152808 |    18259 |     3763 |     2321 |       84 | 25.644 |
c 
c synthesis       73239 conflicts  2129855259 propagations      251 conflicts/sec  7299273 propagations/sec
c Total Memory so far : 704.13Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    114 |     224026 |      39783 |   209622 |    11183 |     3797 |     3763 |      202 | 25.644 |
c |  1 |     28 |     143563 |      35495 |   154008 |    19304 |     3763 |     2321 |       84 | 25.644 |
c 
c synthesis       75278 conflicts  2184790534 propagations      251 conflicts/sec  7289429 propagations/sec
c Total Memory so far : 674.04Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    116 |     226158 |      40769 |   211915 |    12169 |     3797 |     3763 |      204 | 25.644 |
c |  1 |     28 |     144955 |      36462 |   154877 |    10369 |     3763 |     2321 |       88 | 25.644 |
c 
c synthesis       77231 conflicts  2243830135 propagations      251 conflicts/sec  7293315 propagations/sec
c Total Memory so far : 643.94Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    116 |     228087 |      41896 |   212830 |    13296 |     3797 |     3763 |      206 | 25.644 |
c |  1 |     28 |     146433 |      37444 |   156113 |    11350 |     3763 |     2321 |       90 | 25.644 |
c 
c synthesis       79340 conflicts  2300198730 propagations      251 conflicts/sec  7288237 propagations/sec
c Total Memory so far : 643.94Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    116 |     230156 |      42956 |   216269 |    14356 |     3797 |     3763 |      212 | 25.644 |
c |  1 |     28 |     147873 |      38414 |   156974 |    12320 |     3763 |     2321 |       91 | 25.644 |
c 
c synthesis       81370 conflicts  2356470884 propagations      251 conflicts/sec  7283153 propagations/sec
c Total Memory so far : 643.94Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    117 |     232260 |      43929 |   219423 |    15328 |     3797 |     3763 |      221 | 25.644 |
c |  1 |     28 |     149462 |      39428 |   157625 |    13335 |     3763 |     2321 |       91 | 25.644 |
c 
c synthesis       83357 conflicts  2414295389 propagations      251 conflicts/sec  7282929 propagations/sec
c Total Memory so far : 643.94Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    117 |     234378 |      44989 |   222013 |    16389 |     3797 |     3763 |      227 | 25.644 |
c |  1 |     28 |     150750 |      40398 |   158660 |    14304 |     3763 |     2321 |       91 | 25.644 |
c 
c synthesis       85387 conflicts  2472326736 propagations      252 conflicts/sec  7283342 propagations/sec
c Total Memory so far : 643.94Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    117 |     235970 |      46094 |   223517 |    17493 |     3797 |     3763 |      229 | 25.644 |
c |  1 |     28 |     151895 |      41272 |   159485 |    15179 |     3763 |     2321 |       91 | 25.644 |
c 
c synthesis       87366 conflicts  2530127400 propagations      251 conflicts/sec  7283057 propagations/sec
c Total Memory so far : 644.07Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    124 |     241279 |      47065 |   227332 |    18464 |     3839 |     3780 |      238 | 25.644 |
c |  1 |     32 |     154395 |      42121 |   162173 |    16028 |     3810 |     3834 |       97 | 25.644 |
c 
c synthesis       89186 conflicts  2588406384 propagations      251 conflicts/sec  7284142 propagations/sec
c Total Memory so far : 644.07Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    133 |     246114 |      48049 |   231668 |    19448 |     3969 |     3977 |      246 | 25.644 |
c |  1 |     36 |     158332 |      43165 |   167607 |    17072 |     3999 |     3939 |      113 | 25.644 |
c 
c synthesis       91214 conflicts  2644520167 propagations      251 conflicts/sec  7279280 propagations/sec
c Total Memory so far : 644.07Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    136 |     249645 |      49055 |   237730 |    20455 |     4072 |     4182 |      253 | 25.644 |
c |  1 |     42 |     163282 |      44164 |   172968 |    18071 |     4186 |     4069 |      124 | 25.644 |
c 
c synthesis       93219 conflicts  2700738975 propagations      251 conflicts/sec  7274869 propagations/sec
c Total Memory so far : 644.07Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    140 |     253327 |      50057 |   242957 |    21457 |     4225 |     4266 |      261 | 25.644 |
c |  1 |     44 |     166597 |      45091 |   179035 |    18998 |     4281 |     4207 |      129 | 25.644 |
c 
c synthesis       95148 conflicts  2756824107 propagations      251 conflicts/sec  7270321 propagations/sec
c Total Memory so far : 644.20Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    142 |     256119 |      51049 |   246833 |    22449 |     4344 |     4320 |      275 | 25.644 |
c |  1 |     48 |     170103 |      46034 |   185084 |    19941 |     4440 |     4297 |      137 | 25.644 |
c 
c synthesis       97083 conflicts  2814211934 propagations      251 conflicts/sec  7269311 propagations/sec
c Total Memory so far : 644.20Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    143 |     258370 |      51999 |   249622 |    23399 |     4459 |     4611 |      281 | 25.644 |
c |  1 |     57 |     176008 |      47030 |   190316 |    20937 |     4611 |     4457 |      155 | 25.644 |
c 
c synthesis       99029 conflicts  2869031596 propagations      251 conflicts/sec  7261873 propagations/sec
c Total Memory so far : 674.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    148 |     262233 |      52966 |   253815 |    24366 |     4624 |     4737 |      292 | 25.644 |
c |  1 |     62 |     179973 |      47985 |   194967 |    21892 |     4746 |     4558 |      175 | 25.644 |
c 
c synthesis      100951 conflicts  2925037953 propagations      250 conflicts/sec  7257648 propagations/sec
c Total Memory so far : 674.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     267559 |      53875 |   257169 |    25275 |     4766 |     4840 |      303 | 25.644 |
c |  1 |     73 |     186638 |      48904 |   199838 |    22810 |     4883 |     4760 |      196 | 25.644 |
c 
c synthesis      102779 conflicts  2981886983 propagations      250 conflicts/sec  7255580 propagations/sec
c Total Memory so far : 674.43Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     269669 |      54817 |   260024 |    13222 |     4947 |     4840 |      311 | 25.644 |
c |  1 |     79 |     191209 |      49855 |   204323 |    23762 |     5029 |     4897 |      203 | 25.644 |
c 
c synthesis      104672 conflicts  3037174637 propagations      250 conflicts/sec  7250065 propagations/sec
c Total Memory so far : 674.43Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     271594 |      55878 |   262955 |    14283 |     5212 |     4840 |      320 | 25.644 |
c |  1 |     79 |     192576 |      50729 |   206648 |    24636 |     5179 |     4897 |      209 | 25.644 |
c 
c synthesis      106607 conflicts  3093527088 propagations      250 conflicts/sec  7247037 propagations/sec
c Total Memory so far : 674.43Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     273216 |      56948 |   264948 |    15353 |     5503 |     4840 |      331 | 25.644 |
c |  1 |     81 |     194818 |      51681 |   210299 |    13142 |     5355 |     5369 |      229 | 25.644 |
c 
c synthesis      108629 conflicts  3149675299 propagations      250 conflicts/sec  7243928 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     274678 |      57976 |   266642 |    16380 |     5770 |     4840 |      341 | 25.644 |
c |  1 |     81 |     196251 |      52656 |   213608 |    14117 |     5474 |     5369 |      234 | 25.644 |
c 
c synthesis      110632 conflicts  3207578464 propagations      250 conflicts/sec  7244657 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     276360 |      59089 |   267757 |    17494 |     6037 |     4840 |      345 | 25.644 |
c |  1 |     83 |     199336 |      53683 |   217976 |    15145 |     5647 |     5846 |      247 | 25.644 |
c 
c synthesis      112772 conflicts  3264524597 propagations      250 conflicts/sec  7243204 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    156 |     277676 |      60126 |   268768 |    18531 |     6252 |     4840 |      346 | 25.644 |
c |  1 |     87 |     202864 |      54597 |   221938 |    16059 |     5787 |     6236 |      258 | 25.644 |
c 
c synthesis      114723 conflicts  3326500410 propagations      250 conflicts/sec  7252766 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    161 |     281714 |      61136 |   271813 |    19541 |     6397 |     5830 |      353 | 25.644 |
c |  1 |     94 |     207618 |      55619 |   225739 |    17081 |     5916 |     6348 |      273 | 25.644 |
c 
c synthesis      116755 conflicts  3382102345 propagations      250 conflicts/sec  7248372 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    161 |     283535 |      62188 |   273708 |    20593 |     6572 |     5830 |      363 | 25.644 |
c |  1 |     94 |     209330 |      56705 |   227647 |    18167 |     6104 |     6348 |      281 | 25.644 |
c 
c synthesis      118893 conflicts  3437133857 propagations      251 conflicts/sec  7242982 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    161 |     285309 |      63253 |   274920 |    21658 |     6830 |     5830 |      369 | 25.644 |
c |  1 |     94 |     210619 |      57588 |   229695 |    19049 |     6282 |     6348 |      287 | 25.644 |
c 
c synthesis      120841 conflicts  3494884490 propagations      250 conflicts/sec  7243351 propagations/sec
c Total Memory so far : 644.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    162 |     286755 |      64278 |   275818 |    22683 |     7036 |     6432 |      377 | 25.644 |
c |  1 |     94 |     212226 |      58653 |   231288 |    20115 |     6445 |     6348 |      296 | 25.644 |
c 
c synthesis      122931 conflicts  3551275316 propagations      251 conflicts/sec  7240936 propagations/sec
c Total Memory so far : 674.56Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    163 |     288602 |      65360 |   277493 |    23765 |     7176 |     6612 |      393 | 25.644 |
c |  1 |     94 |     214181 |      59736 |   232796 |    21198 |     6613 |     6348 |      307 | 25.644 |
c 
c synthesis      125096 conflicts  3608083565 propagations      251 conflicts/sec  7239432 propagations/sec
c Total Memory so far : 674.69Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    168 |     291628 |      66255 |   281783 |    24660 |     7264 |     6737 |      417 | 25.644 |
c |  1 |     94 |     215550 |      60803 |   233741 |    22264 |     6747 |     6348 |      314 | 25.644 |
c 
c synthesis      127058 conflicts  3664880259 propagations      251 conflicts/sec  7237957 propagations/sec
c Total Memory so far : 674.69Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    171 |     294937 |      67264 |   285636 |    25669 |     7440 |     6866 |      430 | 25.644 |
c |  1 |     94 |     217214 |      61881 |   235648 |    23343 |     6881 |     6348 |      322 | 25.644 |
c 
c synthesis      129145 conflicts  3720548523 propagations      251 conflicts/sec  7234297 propagations/sec
c Total Memory so far : 674.69Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    178 |     298518 |      68194 |   288532 |    26599 |     7579 |     7034 |      447 | 25.644 |
c |  1 |     94 |     218984 |      62965 |   236989 |    24427 |     7044 |     6348 |      332 | 25.644 |
c 
c synthesis      131159 conflicts  3775435399 propagations      251 conflicts/sec  7229268 propagations/sec
c Total Memory so far : 674.69Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    187 |     304547 |      69059 |   292185 |    27464 |     7669 |     7191 |      460 | 25.644 |
c |  1 |     94 |     220868 |      64050 |   239377 |    25512 |     7196 |     6348 |      335 | 25.644 |
c 
c synthesis      133109 conflicts  3827387177 propagations      251 conflicts/sec  7218876 propagations/sec
c Total Memory so far : 674.82Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    188 |     306397 |      69999 |   294980 |    28403 |     7881 |     7204 |      474 | 25.644 |
c |  1 |     94 |     222330 |      65087 |   240316 |    26548 |     7364 |     6348 |      339 | 25.644 |
c 
c synthesis      135086 conflicts  3885837839 propagations      251 conflicts/sec  7220818 propagations/sec
c Total Memory so far : 674.82Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    188 |     307842 |      70999 |   296491 |    29404 |     7885 |     7204 |      479 | 25.644 |
c |  1 |     94 |     223872 |      66080 |   240957 |    27542 |     7365 |     6348 |      343 | 25.644 |
c 
c synthesis      137079 conflicts  3944230472 propagations      251 conflicts/sec  7222611 propagations/sec
c Total Memory so far : 674.82Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    188 |     309048 |      71903 |   297588 |    30308 |     7885 |     7204 |      489 | 25.644 |
c |  1 |     94 |     225265 |      67086 |   241969 |    28548 |     7365 |     6348 |      345 | 25.644 |
c 
c synthesis      138989 conflicts  4000995764 propagations      251 conflicts/sec  7221433 propagations/sec
c Total Memory so far : 674.82Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    188 |     310654 |      72822 |   299239 |    15630 |     7885 |     7204 |      495 | 25.644 |
c |  1 |     94 |     226760 |      68089 |   242643 |    29551 |     7365 |     6348 |      350 | 25.644 |
c 
c synthesis      140911 conflicts  4059978911 propagations      251 conflicts/sec  7224428 propagations/sec
c Total Memory so far : 674.82Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    188 |     312060 |      73750 |   300619 |    16557 |     7885 |     7204 |      498 | 25.644 |
c |  1 |     94 |     228162 |      69089 |   243306 |    15527 |     7365 |     6348 |      356 | 25.644 |
c 
c synthesis      142839 conflicts  4117413983 propagations      251 conflicts/sec  7224591 propagations/sec
c Total Memory so far : 644.86Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     314433 |      74847 |   303058 |    17654 |     7885 |     7365 |      515 | 25.644 |
c |  1 |     94 |     229406 |      70084 |   243660 |    16522 |     7365 |     6348 |      358 | 25.644 |
c 
c synthesis      144931 conflicts  4173573787 propagations      251 conflicts/sec  7222410 propagations/sec
c Total Memory so far : 644.86Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     316071 |      75931 |   304559 |    18739 |     7885 |     7365 |      528 | 25.644 |
c |  1 |     94 |     230638 |      71089 |   244053 |    17526 |     7365 |     6348 |      361 | 25.644 |
c 
c synthesis      147020 conflicts  4232597033 propagations      251 conflicts/sec  7225171 propagations/sec
c Total Memory so far : 644.86Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     317590 |      76931 |   306490 |    19739 |     7885 |     7365 |      538 | 25.644 |
c |  1 |     94 |     232011 |      72071 |   245025 |    18509 |     7365 |     6348 |      367 | 25.644 |
c 
c synthesis      149002 conflicts  4290906937 propagations      251 conflicts/sec  7226620 propagations/sec
c Total Memory so far : 644.86Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     319328 |      77929 |   308400 |    20737 |     7885 |     7365 |      548 | 25.644 |
c |  1 |     94 |     233242 |      73051 |   245499 |    19488 |     7365 |     6348 |      369 | 25.644 |
c 
c synthesis      150980 conflicts  4349595489 propagations      251 conflicts/sec  7228678 propagations/sec
c Total Memory so far : 644.86Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     320835 |      79006 |   309740 |    21814 |     7885 |     7365 |      555 | 25.644 |
c |  1 |     94 |     234564 |      74053 |   246461 |    20491 |     7365 |     6348 |      373 | 25.644 |
c 
c synthesis      153059 conflicts  4405806813 propagations      251 conflicts/sec  7226647 propagations/sec
c Total Memory so far : 674.95Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     322344 |      80019 |   310751 |    22827 |     7885 |     7365 |      562 | 25.644 |
c |  1 |     94 |     235824 |      75013 |   247255 |    21451 |     7365 |     6348 |      376 | 25.644 |
c 
c synthesis      155032 conflicts  4461908128 propagations      251 conflicts/sec  7224453 propagations/sec
c Total Memory so far : 674.95Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     323667 |      80992 |   311621 |    23799 |     7885 |     7365 |      565 | 25.644 |
c |  1 |     94 |     237159 |      75973 |   247938 |    22411 |     7365 |     6348 |      380 | 25.644 |
c 
c synthesis      156965 conflicts  4518329827 propagations      251 conflicts/sec  7222871 propagations/sec
c Total Memory so far : 674.95Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     325257 |      82023 |   312602 |    24831 |     7885 |     7365 |      575 | 25.644 |
c |  1 |     94 |     238472 |      76964 |   248373 |    23402 |     7365 |     6348 |      386 | 25.644 |
c 
c synthesis      158987 conflicts  4577518172 propagations      251 conflicts/sec  7225661 propagations/sec
c Total Memory so far : 675.08Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     327285 |      83159 |   314290 |    25967 |     7885 |     7365 |      590 | 25.644 |
c |  1 |     94 |     239642 |      77956 |   248584 |    24394 |     7365 |     6348 |      387 | 25.644 |
c 
c synthesis      161115 conflicts  4633832751 propagations      251 conflicts/sec  7223890 propagations/sec
c Total Memory so far : 675.08Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     329055 |      84204 |   315894 |    27011 |     7885 |     7365 |      605 | 25.644 |
c |  1 |     94 |     240841 |      78913 |   248956 |    25351 |     7365 |     6348 |      391 | 25.644 |
c 
c synthesis      163117 conflicts  4687943784 propagations      251 conflicts/sec  7218804 propagations/sec
c Total Memory so far : 675.08Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     330822 |      85233 |   317359 |    28040 |     7885 |     7365 |      614 | 25.644 |
c |  1 |     94 |     241981 |      79859 |   249241 |    26297 |     7365 |     6348 |      393 | 25.644 |
c 
c synthesis      165092 conflicts  4744226213 propagations      251 conflicts/sec  7217124 propagations/sec
c Total Memory so far : 675.08Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     332529 |      86251 |   318445 |    29059 |     7885 |     7365 |      618 | 25.644 |
c |  1 |     94 |     243161 |      80770 |   249734 |    27208 |     7365 |     6348 |      395 | 25.644 |
c 
c synthesis      167021 conflicts  4801612054 propagations      251 conflicts/sec  7217153 propagations/sec
c Total Memory so far : 675.08Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     334016 |      87259 |   319397 |    30067 |     7885 |     7365 |      619 | 25.644 |
c |  1 |     94 |     244382 |      81728 |   250082 |    28166 |     7365 |     6348 |      404 | 25.644 |
c 
c synthesis      168987 conflicts  4856383403 propagations      251 conflicts/sec  7213277 propagations/sec
c Total Memory so far : 675.22Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     335398 |      88236 |   320328 |    31044 |     7885 |     7365 |      625 | 25.644 |
c |  1 |     94 |     246043 |      82851 |   251363 |    29289 |     7365 |     6348 |      413 | 25.644 |
c 
c synthesis      171087 conflicts  4911159065 propagations      251 conflicts/sec  7209525 propagations/sec
c Total Memory so far : 675.22Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     336697 |      89170 |   321219 |    31978 |     7885 |     7365 |      628 | 25.644 |
c |  1 |     94 |     247473 |      83857 |   252370 |    30295 |     7365 |     6348 |      421 | 25.644 |
c 
c synthesis      173027 conflicts  4964645850 propagations      251 conflicts/sec  7203957 propagations/sec
c Total Memory so far : 675.36Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     338053 |      90140 |   322084 |    32948 |     7885 |     7365 |      634 | 25.644 |
c |  1 |     94 |     248942 |      84864 |   253722 |    31301 |     7365 |     6348 |      424 | 25.644 |
c 
c synthesis      175004 conflicts  5019534313 propagations      251 conflicts/sec  7200581 propagations/sec
c Total Memory so far : 675.36Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     339453 |      91031 |   322759 |    33839 |     7885 |     7365 |      639 | 25.644 |
c |  1 |     94 |     251058 |      85887 |   256000 |    32324 |     7365 |     6348 |      427 | 25.644 |
c 
c synthesis      176918 conflicts  5073253704 propagations      251 conflicts/sec  7195565 propagations/sec
c Total Memory so far : 705.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     340549 |      91922 |   323270 |    34730 |     7885 |     7365 |      640 | 25.644 |
c |  1 |     94 |     252485 |      86915 |   256811 |    33353 |     7365 |     6348 |      432 | 25.644 |
c 
c synthesis      178837 conflicts  5125364973 propagations      251 conflicts/sec  7188422 propagations/sec
c Total Memory so far : 705.46Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     342037 |      92897 |   324109 |    35705 |     7930 |     7365 |      646 | 25.644 |
c |  1 |    100 |     256320 |      87888 |   259489 |    34325 |     7428 |     7929 |      441 | 25.644 |
c 
c synthesis      180785 conflicts  5179254186 propagations      251 conflicts/sec  7183891 propagations/sec
c Total Memory so far : 705.59Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     343453 |      93861 |   325012 |    18475 |     8024 |     7365 |      651 | 25.644 |
c |  1 |    102 |     260208 |      88829 |   263163 |    17651 |     7632 |     7987 |      465 | 25.644 |
c 
c synthesis      182690 conflicts  5233775279 propagations      251 conflicts/sec  7180612 propagations/sec
c Total Memory so far : 645.39Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     344663 |      94769 |   325677 |    19383 |     8143 |     7365 |      655 | 25.644 |
c |  1 |    107 |     265420 |      89840 |   267367 |    18662 |     7705 |     8132 |      477 | 25.644 |
c 
c synthesis      184609 conflicts  5288646433 propagations      251 conflicts/sec  7177624 propagations/sec
c Total Memory so far : 645.39Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     346048 |      95705 |   326591 |    20319 |     8251 |     7365 |      661 | 25.644 |
c |  1 |    110 |     268814 |      90848 |   271248 |    19670 |     7823 |     8154 |      495 | 25.644 |
c 
c synthesis      186553 conflicts  5344668913 propagations      250 conflicts/sec  7176239 propagations/sec
c Total Memory so far : 645.39Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     347307 |      96625 |   326990 |    21239 |     8412 |     7365 |      662 | 25.644 |
c |  1 |    110 |     270430 |      91814 |   273388 |    20636 |     7924 |     8154 |      498 | 25.644 |
c 
c synthesis      188439 conflicts  5401967494 propagations      250 conflicts/sec  7176582 propagations/sec
c Total Memory so far : 645.39Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     348502 |      97574 |   327433 |    22188 |     8501 |     7365 |      666 | 25.644 |
c |  1 |    110 |     271890 |      92795 |   274619 |    21616 |     8032 |     8154 |      504 | 25.644 |
c 
c synthesis      190369 conflicts  5459828831 propagations      250 conflicts/sec  7177644 propagations/sec
c Total Memory so far : 645.39Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     349769 |      98523 |   327864 |    23137 |     8628 |     7365 |      674 | 25.644 |
c |  1 |    110 |     273660 |      93766 |   276687 |    22588 |     8134 |     8154 |      516 | 25.644 |
c 
c synthesis      192289 conflicts  5517334016 propagations      250 conflicts/sec  7178223 propagations/sec
c Total Memory so far : 645.39Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    189 |     351142 |      99510 |   328532 |    24124 |     8782 |     7365 |      680 | 25.644 |
c |  1 |    114 |     276551 |      94606 |   279957 |    23428 |     8223 |     8770 |      529 | 25.644 |
c 
c synthesis      194116 conflicts  5573398515 propagations      250 conflicts/sec  7176964 propagations/sec
c Total Memory so far : 675.49Mb
c
c Try to adapt solver strategies
c 
c Nothing extreme in this problem, continue with glucose default strategies.
c
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     354247 |     100479 |   329741 |    25091 |     8906 |     8376 |      691 | 25.644 |
c |  1 |    120 |     281036 |      95573 |   283257 |    24394 |     8379 |     8872 |      557 | 25.644 |
c 
c synthesis      196052 conflicts  5629209995 propagations      250 conflicts/sec  7175357 propagations/sec
c Total Memory so far : 675.62Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     355788 |     101451 |   331100 |    26064 |     9018 |     8376 |      708 | 25.644 |
c |  1 |    126 |     285221 |      96549 |   286696 |    25371 |     8508 |     9013 |      588 | 25.644 |
c 
c synthesis      198000 conflicts  5682693085 propagations      250 conflicts/sec  7170860 propagations/sec
c Total Memory so far : 675.62Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     357325 |     102427 |   332535 |    27040 |     9110 |     8376 |      719 | 25.644 |
c |  1 |    127 |     287772 |      97397 |   290226 |    26219 |     8679 |     9092 |      605 | 25.644 |
c 
c synthesis      199824 conflicts  5734801822 propagations      250 conflicts/sec  7164747 propagations/sec
c Total Memory so far : 675.62Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     358631 |     103324 |   333313 |    27937 |     9199 |     8376 |      727 | 25.644 |
c |  1 |    130 |     290637 |      98395 |   293590 |    27217 |     8873 |     9182 |      621 | 25.644 |
c 
c synthesis      201719 conflicts  5788784781 propagations      250 conflicts/sec  7161071 propagations/sec
c Total Memory so far : 675.62Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     359888 |     104210 |   335043 |    28822 |     9329 |     8376 |      741 | 25.644 |
c |  1 |    130 |     292673 |      99390 |   295736 |    28211 |     9002 |     9182 |      640 | 25.644 |
c 
c synthesis      203600 conflicts  5840302220 propagations      249 conflicts/sec  7154435 propagations/sec
c Total Memory so far : 675.62Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     361618 |     105202 |   336616 |    29814 |     9480 |     8376 |      750 | 25.644 |
c |  1 |    130 |     294812 |     100391 |   297688 |    29213 |     9126 |     9182 |      659 | 25.644 |
c 
c synthesis      205593 conflicts  5890763276 propagations      249 conflicts/sec  7146635 propagations/sec
c Total Memory so far : 675.62Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    194 |     363046 |     106162 |   338035 |    30775 |     9669 |     8376 |      755 | 25.644 |
c |  1 |    130 |     296404 |     101406 |   299160 |    30228 |     9269 |     9182 |      667 | 25.644 |
c 
c synthesis      207568 conflicts  5943439844 propagations      249 conflicts/sec  7141665 propagations/sec
c Total Memory so far : 675.75Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    200 |     366251 |     107077 |   339925 |    31690 |     9792 |     9425 |      776 | 25.644 |
c |  1 |    131 |     298162 |     102391 |   301186 |    31213 |     9436 |     9699 |      680 | 25.644 |
c 
c synthesis      209468 conflicts  6000684721 propagations      249 conflicts/sec  7142238 propagations/sec
c Total Memory so far : 675.75Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    202 |     368774 |     108061 |   341499 |    32674 |     9911 |     9447 |      799 | 25.644 |
c |  1 |    131 |     299901 |     103333 |   303848 |    32155 |     9609 |     9699 |      683 | 25.644 |
c 
c synthesis      211394 conflicts  6057359035 propagations      249 conflicts/sec  7142130 propagations/sec
c Total Memory so far : 705.84Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    203 |     370799 |     109084 |   343719 |    33697 |    10142 |     9617 |      842 | 25.644 |
c |  1 |    131 |     301755 |     104248 |   306057 |    33070 |     9785 |     9699 |      691 | 25.644 |
c 
c synthesis      213332 conflicts  6115804828 propagations      249 conflicts/sec  7144083 propagations/sec
c Total Memory so far : 705.84Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    203 |     372043 |     109981 |   344688 |    34594 |    10343 |     9617 |      855 | 25.644 |
c |  1 |    131 |     303292 |     105174 |   308197 |    33996 |     9957 |     9699 |      699 | 25.644 |
c 
c synthesis      215155 conflicts  6173044917 propagations      249 conflicts/sec  7144582 propagations/sec
c Total Memory so far : 705.84Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 |    203 |     373554 |     110992 |   345801 |    35605 |    10499 |     9617 |      869 | 25.644 |
c |  1 |    131 |     304741 |     105981 |   309662 |    34803 |    10067 |     9699 |      703 | 25.644 |
...
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129548 |  320544165 |  193975660 |  1465787 |  1516210 |  8194313 |  8265588 |  4082385 | 29.515 |
c |  1 | 3174627 |  326294812 |  195618614 |  1471962 |  1415378 |  8265593 |  8194309 |  3978640 | 29.515 |
c 
c synthesis   389594274 conflicts 15197992701944 propagations       70 conflicts/sec  2743195 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129555 |  320544654 |  193976018 |  1465787 |  1516568 |  8194454 |  8265679 |  4082430 | 29.515 |
c |  1 | 3174633 |  326295267 |  195618929 |  1471962 |  1415694 |  8265683 |  8194437 |  3978683 | 29.515 |
c 
c synthesis   389594947 conflicts 15198018143735 propagations       70 conflicts/sec  2743195 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129562 |  320545117 |  193976345 |  1465787 |  1516895 |  8194551 |  8265791 |  4082470 | 29.515 |
c |  1 | 3174640 |  326295783 |  195619276 |  1471962 |  1416041 |  8265791 |  8194546 |  3978714 | 29.515 |
c 
c synthesis   389595621 conflicts 15198046002933 propagations       70 conflicts/sec  2743196 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129568 |  320545589 |  193976683 |  1465787 |  1517233 |  8194679 |  8265912 |  4082499 | 29.515 |
c |  1 | 3174648 |  326296388 |  195619682 |  1471962 |  1416447 |  8265917 |  8194673 |  3978750 | 29.515 |
c 
c synthesis   389596365 conflicts 15198078588779 propagations       70 conflicts/sec  2743198 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129575 |  320546098 |  193977054 |  1465787 |  1517604 |  8194781 |  8266040 |  4082533 | 29.515 |
c |  1 | 3174655 |  326296877 |  195620024 |  1471962 |  1416789 |  8266042 |  8194779 |  3978790 | 29.515 |
c 
c synthesis   389597078 conflicts 15198107271990 propagations       70 conflicts/sec  2743199 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129583 |  320546633 |  193977414 |  1465787 |  1517964 |  8194870 |  8266160 |  4082559 | 29.515 |
c |  1 | 3174662 |  326297378 |  195620386 |  1471962 |  1417151 |  8266163 |  8194864 |  3978828 | 29.515 |
c 
c synthesis   389597800 conflicts 15198134757967 propagations       70 conflicts/sec  2743200 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129589 |  320547125 |  193977741 |  1465787 |  1518291 |  8194935 |  8266282 |  4082575 | 29.515 |
c |  1 | 3174668 |  326297835 |  195620721 |  1471962 |  1417486 |  8266293 |  8194923 |  3978854 | 29.515 |
c 
c synthesis   389598462 conflicts 15198163560850 propagations       70 conflicts/sec  2743202 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129596 |  320547647 |  193978110 |  1465787 |  1518660 |  8195046 |  8266421 |  4082610 | 29.515 |
c |  1 | 3174675 |  326298320 |  195621045 |  1471962 |  1417810 |  8266426 |  8195044 |  3978891 | 29.515 |
c 
c synthesis   389599155 conflicts 15198190884350 propagations       70 conflicts/sec  2743203 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129603 |  320548136 |  193978460 |  1465787 |  1519010 |  8195177 |  8266521 |  4082635 | 29.515 |
c |  1 | 3174681 |  326298784 |  195621366 |  1471962 |  1418131 |  8266536 |  8195171 |  3978920 | 29.515 |
c 
c synthesis   389599826 conflicts 15198217065974 propagations       70 conflicts/sec  2743204 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129610 |  320548641 |  193978830 |  1465787 |  1519380 |  8195289 |  8266666 |  4082681 | 29.515 |
c |  1 | 3174688 |  326299287 |  195621723 |  1471962 |  1418487 |  8266690 |  8195285 |  3978955 | 29.515 |
c 
c synthesis   389600553 conflicts 15198245286831 propagations       70 conflicts/sec  2743205 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129617 |  320549143 |  193979160 |  1465787 |  1519710 |  8195379 |  8266808 |  4082711 | 29.515 |
c |  1 | 3174694 |  326299757 |  195622048 |  1471962 |  1418813 |  8266819 |  8195376 |  3978984 | 29.515 |
c 
c synthesis   389601208 conflicts 15198271223501 propagations       70 conflicts/sec  2743205 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129623 |  320549647 |  193979487 |  1465787 |  1520037 |  8195461 |  8266945 |  4082728 | 29.515 |
c |  1 | 3174700 |  326300169 |  195622358 |  1471962 |  1419123 |  8266966 |  8195448 |  3979007 | 29.515 |
c 
c synthesis   389601845 conflicts 15198296775127 propagations       70 conflicts/sec  2743206 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129630 |  320550171 |  193979841 |  1465787 |  1520391 |  8195527 |  8267099 |  4082746 | 29.515 |
c |  1 | 3174707 |  326300705 |  195622705 |  1471962 |  1419470 |  8267102 |  8195511 |  3979030 | 29.515 |
c 
c synthesis   389602546 conflicts 15198325220475 propagations       70 conflicts/sec  2743207 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129638 |  320550716 |  193980215 |  1465787 |  1520765 |  8195634 |  8267228 |  4082778 | 29.515 |
c |  1 | 3174713 |  326301124 |  195623021 |  1471962 |  1419786 |  8267234 |  8195611 |  3979060 | 29.515 |
c 
c synthesis   389603236 conflicts 15198352550505 propagations       70 conflicts/sec  2743208 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129644 |  320551167 |  193980535 |  1465787 |  1521085 |  8195761 |  8267379 |  4082814 | 29.515 |
c |  1 | 3174721 |  326301669 |  195623382 |  1471962 |  1420146 |  8267381 |  8195759 |  3979085 | 29.515 |
c 
c synthesis   389603917 conflicts 15198378818598 propagations       70 conflicts/sec  2743209 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129651 |  320551612 |  193980876 |  1465787 |  1521426 |  8195888 |  8267522 |  4082872 | 29.515 |
c |  1 | 3174727 |  326302079 |  195623687 |  1471963 |  1420452 |  8267523 |  8195886 |  3979111 | 29.515 |
c 
c synthesis   389604563 conflicts 15198404482369 propagations       70 conflicts/sec  2743210 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129658 |  320552129 |  193981264 |  1465787 |  1521814 |  8196049 |  8267679 |  4082956 | 29.515 |
c |  1 | 3174734 |  326302569 |  195624067 |  1471963 |  1420832 |  8267703 |  8196042 |  3979158 | 29.515 |
c 
c synthesis   389605331 conflicts 15198432806278 propagations       70 conflicts/sec  2743211 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129665 |  320552603 |  193981602 |  1465787 |  1522152 |  8196199 |  8267782 |  4083010 | 29.515 |
c |  1 | 3174742 |  326303137 |  195624458 |  1471963 |  1421223 |  8267786 |  8196198 |  3979191 | 29.515 |
c 
c synthesis   389606060 conflicts 15198461565813 propagations       70 conflicts/sec  2743212 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129671 |  320553089 |  193981920 |  1465787 |  1522470 |  8196285 |  8267861 |  4083039 | 29.515 |
c |  1 | 3174749 |  326303711 |  195624840 |  1471963 |  1421605 |  8267866 |  8196277 |  3979215 | 29.515 |
c 
c synthesis   389606760 conflicts 15198489205198 propagations       70 conflicts/sec  2743213 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129677 |  320553503 |  193982226 |  1465787 |  1522776 |  8196438 |  8267948 |  4083073 | 29.515 |
c |  1 | 3174756 |  326304259 |  195625211 |  1471963 |  1421976 |  8267954 |  8196423 |  3979242 | 29.515 |
c 
c synthesis   389607437 conflicts 15198517719161 propagations       70 conflicts/sec  2743214 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129684 |  320553965 |  193982548 |  1465787 |  1523098 |  8196599 |  8268019 |  4083104 | 29.515 |
c |  1 | 3174763 |  326304737 |  195625535 |  1471963 |  1422300 |  8268019 |  8196589 |  3979289 | 29.515 |
c 
c synthesis   389608083 conflicts 15198543708103 propagations       70 conflicts/sec  2743215 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129691 |  320554463 |  193982907 |  1465788 |  1523457 |  8196717 |  8268108 |  4083129 | 29.515 |
c |  1 | 3174771 |  326305314 |  195625930 |  1471963 |  1422695 |  8268111 |  8196713 |  3979330 | 29.515 |
c 
c synthesis   389608837 conflicts 15198572586773 propagations       70 conflicts/sec  2743216 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129698 |  320555018 |  193983273 |  1465788 |  1523823 |  8196802 |  8268209 |  4083155 | 29.515 |
c |  1 | 3174776 |  326305688 |  195626209 |  1471963 |  1422974 |  8268217 |  8196797 |  3979362 | 29.515 |
c 
c synthesis   389609482 conflicts 15198598150794 propagations       70 conflicts/sec  2743217 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129704 |  320555426 |  193983596 |  1465788 |  1524146 |  8196941 |  8268304 |  4083187 | 29.515 |
c |  1 | 3174783 |  326306202 |  195626568 |  1471963 |  1423333 |  8268322 |  8196917 |  3979392 | 29.515 |
c 
c synthesis   389610164 conflicts 15198624293616 propagations       70 conflicts/sec  2743218 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129711 |  320555991 |  193983927 |  1465788 |  1524477 |  8197085 |  8268457 |  4083225 | 29.515 |
c |  1 | 3174789 |  326306684 |  195626877 |  1471963 |  1423642 |  8268459 |  8197078 |  3979436 | 29.515 |
c 
c synthesis   389610804 conflicts 15198648764955 propagations       70 conflicts/sec  2743218 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129718 |  320556499 |  193984286 |  1465788 |  1524836 |  8197211 |  8268618 |  4083254 | 29.515 |
c |  1 | 3174797 |  326307228 |  195627269 |  1471963 |  1424034 |  8268622 |  8197200 |  3979469 | 29.515 |
c 
c synthesis   389611555 conflicts 15198675717756 propagations       70 conflicts/sec  2743219 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129725 |  320557031 |  193984656 |  1465788 |  1525206 |  8197294 |  8268700 |  4083269 | 29.515 |
c |  1 | 3174804 |  326307759 |  195627615 |  1471963 |  1424380 |  8268708 |  8197288 |  3979489 | 29.515 |
c 
c synthesis   389612271 conflicts 15198706555486 propagations       70 conflicts/sec  2743221 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129732 |  320557494 |  193984986 |  1465788 |  1525536 |  8197384 |  8268835 |  4083300 | 29.515 |
c |  1 | 3174811 |  326308239 |  195627959 |  1471963 |  1424724 |  8268835 |  8197383 |  3979525 | 29.515 |
c 
c synthesis   389612945 conflicts 15198733523954 propagations       70 conflicts/sec  2743222 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129739 |  320558054 |  193985386 |  1465788 |  1525936 |  8197488 |  8268950 |  4083325 | 29.515 |
c |  1 | 3174817 |  326308670 |  195628261 |  1471963 |  1425026 |  8268970 |  8197487 |  3979544 | 29.515 |
c 
c synthesis   389613647 conflicts 15198761017944 propagations       70 conflicts/sec  2743223 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129746 |  320558562 |  193985737 |  1465788 |  1526287 |  8197618 |  8269052 |  4083373 | 29.515 |
c |  1 | 3174823 |  326309150 |  195628603 |  1471963 |  1425367 |  8269075 |  8197607 |  3979571 | 29.515 |
c 
c synthesis   389614340 conflicts 15198788193748 propagations       70 conflicts/sec  2743224 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129753 |  320559049 |  193986080 |  1465788 |  1526630 |  8197729 |  8269140 |  4083412 | 29.515 |
c |  1 | 3174830 |  326309696 |  195628964 |  1471963 |  1425729 |  8269152 |  8197710 |  3979606 | 29.515 |
c 
c synthesis   389615044 conflicts 15198816149507 propagations       70 conflicts/sec  2743225 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129761 |  320559590 |  193986458 |  1465788 |  1527008 |  8197821 |  8269295 |  4083436 | 29.515 |
c |  1 | 3174838 |  326310210 |  195629338 |  1471963 |  1426103 |  8269298 |  8197821 |  3979630 | 29.515 |
c 
c synthesis   389615796 conflicts 15198845926568 propagations       70 conflicts/sec  2743226 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129768 |  320560162 |  193986854 |  1465788 |  1527403 |  8197929 |  8269400 |  4083465 | 29.515 |
c |  1 | 3174845 |  326310727 |  195629710 |  1471963 |  1426475 |  8269407 |  8197925 |  3979658 | 29.515 |
c 
c synthesis   389616564 conflicts 15198877891371 propagations       70 conflicts/sec  2743228 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129776 |  320560683 |  193987218 |  1465788 |  1527768 |  8198071 |  8269517 |  4083494 | 29.515 |
c |  1 | 3174852 |  326311251 |  195630077 |  1471963 |  1426842 |  8269518 |  8198056 |  3979694 | 29.515 |
c 
c synthesis   389617295 conflicts 15198907004855 propagations       70 conflicts/sec  2743229 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129782 |  320561161 |  193987564 |  1465788 |  1528114 |  8198211 |  8269618 |  4083513 | 29.515 |
c |  1 | 3174860 |  326311783 |  195630463 |  1471963 |  1427228 |  8269639 |  8198203 |  3979714 | 29.515 |
c 
c synthesis   389618027 conflicts 15198935353269 propagations       70 conflicts/sec  2743231 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129790 |  320561730 |  193987948 |  1465788 |  1528498 |  8198297 |  8269739 |  4083539 | 29.515 |
c |  1 | 3174867 |  326312289 |  195630801 |  1471963 |  1427566 |  8269741 |  8198295 |  3979757 | 29.515 |
c 
c synthesis   389618749 conflicts 15198963762964 propagations       70 conflicts/sec  2743232 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129797 |  320562226 |  193988298 |  1465788 |  1528848 |  8198423 |  8269862 |  4083573 | 29.515 |
c |  1 | 3174873 |  326312763 |  195631129 |  1471963 |  1427894 |  8269868 |  8198411 |  3979791 | 29.515 |
c 
c synthesis   389619427 conflicts 15198991769352 propagations       70 conflicts/sec  2743233 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129803 |  320562673 |  193988620 |  1465788 |  1529170 |  8198528 |  8269932 |  4083592 | 29.515 |
c |  1 | 3174880 |  326313286 |  195631486 |  1471964 |  1428251 |  8269935 |  8198522 |  3979818 | 29.515 |
c 
c synthesis   389620106 conflicts 15199021104942 propagations       70 conflicts/sec  2743234 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129810 |  320563212 |  193988989 |  1465788 |  1529539 |  8198626 |  8270014 |  4083623 | 29.515 |
c |  1 | 3174886 |  326313724 |  195631789 |  1471964 |  1428554 |  8270024 |  8198612 |  3979843 | 29.515 |
c 
c synthesis   389620778 conflicts 15199049031258 propagations       70 conflicts/sec  2743235 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129817 |  320563703 |  193989337 |  1465788 |  1529887 |  8198766 |  8270089 |  4083651 | 29.515 |
c |  1 | 3174893 |  326314272 |  195632136 |  1471964 |  1428901 |  8270092 |  8198763 |  3979874 | 29.515 |
c 
c synthesis   389621473 conflicts 15199077753998 propagations       70 conflicts/sec  2743237 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129823 |  320564157 |  193989633 |  1465788 |  1530183 |  8198827 |  8270198 |  4083678 | 29.515 |
c |  1 | 3174899 |  326314706 |  195632472 |  1471964 |  1429237 |  8270223 |  8198820 |  3979902 | 29.515 |
c 
c synthesis   389622105 conflicts 15199103616860 propagations       70 conflicts/sec  2743237 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129830 |  320564667 |  193989982 |  1465788 |  1530532 |  8198942 |  8270361 |  4083716 | 29.515 |
c |  1 | 3174906 |  326315188 |  195632791 |  1471964 |  1429556 |  8270366 |  8198942 |  3979940 | 29.515 |
c 
c synthesis   389622773 conflicts 15199130194237 propagations       70 conflicts/sec  2743238 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129838 |  320565229 |  193990372 |  1465788 |  1530922 |  8199061 |  8270458 |  4083749 | 29.515 |
c |  1 | 3174913 |  326315766 |  195633170 |  1471965 |  1429935 |  8270458 |  8199059 |  3979982 | 29.515 |
c 
c synthesis   389623542 conflicts 15199160478136 propagations       70 conflicts/sec  2743240 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129844 |  320565749 |  193990718 |  1465788 |  1531268 |  8199182 |  8270539 |  4083776 | 29.515 |
c |  1 | 3174920 |  326316264 |  195633513 |  1471965 |  1430278 |  8270549 |  8199174 |  3980016 | 29.515 |
c 
c synthesis   389624231 conflicts 15199188572356 propagations       70 conflicts/sec  2743241 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129850 |  320566161 |  193991017 |  1465788 |  1531567 |  8199332 |  8270634 |  4083807 | 29.515 |
c |  1 | 3174926 |  326316695 |  195633822 |  1471965 |  1430587 |  8270657 |  8199329 |  3980037 | 29.515 |
c 
c synthesis   389624839 conflicts 15199212713793 propagations       70 conflicts/sec  2743241 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129857 |  320566691 |  193991382 |  1465788 |  1531932 |  8199453 |  8270772 |  4083832 | 29.515 |
c |  1 | 3174934 |  326317301 |  195634236 |  1471965 |  1431000 |  8270796 |  8199440 |  3980074 | 29.515 |
c 
c synthesis   389625618 conflicts 15199243721235 propagations       70 conflicts/sec  2743243 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129864 |  320567152 |  193991696 |  1465788 |  1532246 |  8199577 |  8270901 |  4083867 | 29.515 |
c |  1 | 3174941 |  326317825 |  195634593 |  1471965 |  1431358 |  8270901 |  8199567 |  3980092 | 29.515 |
c 
c synthesis   389626289 conflicts 15199272987350 propagations       70 conflicts/sec  2743244 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129871 |  320567683 |  193992078 |  1465788 |  1532628 |  8199732 |  8271025 |  4083902 | 29.515 |
c |  1 | 3174948 |  326318332 |  195634956 |  1471965 |  1431721 |  8271041 |  8199726 |  3980120 | 29.515 |
c 
c synthesis   389627034 conflicts 15199301686180 propagations       70 conflicts/sec  2743246 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129878 |  320568187 |  193992430 |  1465788 |  1532980 |  8199823 |  8271130 |  4083923 | 29.515 |
c |  1 | 3174955 |  326318884 |  195635323 |  1471965 |  1432088 |  8271135 |  8199816 |  3980153 | 29.515 |
c 
c synthesis   389627753 conflicts 15199332301709 propagations       70 conflicts/sec  2743247 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129886 |  320568784 |  193992825 |  1465788 |  1533375 |  8199931 |  8271268 |  4083940 | 29.515 |
c |  1 | 3174963 |  326319472 |  195635730 |  1471965 |  1432495 |  8271278 |  8199925 |  3980201 | 29.515 |
c 
c synthesis   389628555 conflicts 15199364187216 propagations       70 conflicts/sec  2743249 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129893 |  320569330 |  193993210 |  1465788 |  1533760 |  8200034 |  8271412 |  4083987 | 29.515 |
c |  1 | 3174971 |  326320014 |  195636107 |  1471965 |  1432872 |  8271423 |  8200027 |  3980230 | 29.515 |
c 
c synthesis   389629317 conflicts 15199393396212 propagations       70 conflicts/sec  2743250 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129900 |  320569847 |  193993569 |  1465788 |  1534118 |  8200148 |  8271513 |  4084013 | 29.515 |
c |  1 | 3174978 |  326320549 |  195636460 |  1471965 |  1433225 |  8271518 |  8200147 |  3980268 | 29.515 |
c 
c synthesis   389630029 conflicts 15199423298334 propagations       70 conflicts/sec  2743252 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129908 |  320570426 |  193993960 |  1465788 |  1534510 |  8200281 |  8271594 |  4084067 | 29.515 |
c |  1 | 3174985 |  326321125 |  195636855 |  1471965 |  1433620 |  8271612 |  8200263 |  3980326 | 29.515 |
c 
c synthesis   389630815 conflicts 15199455256933 propagations       70 conflicts/sec  2743254 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129914 |  320570853 |  193994279 |  1465788 |  1534829 |  8200396 |  8271730 |  4084112 | 29.515 |
c |  1 | 3174993 |  326321651 |  195637218 |  1471965 |  1433983 |  8271741 |  8200396 |  3980368 | 29.515 |
c 
c synthesis   389631497 conflicts 15199482787447 propagations       70 conflicts/sec  2743255 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129921 |  320571277 |  193994603 |  1465788 |  1535152 |  8200563 |  8271827 |  4084165 | 29.515 |
c |  1 | 3175001 |  326322268 |  195637653 |  1471965 |  1434418 |  8271832 |  8200546 |  3980413 | 29.515 |
c 
c synthesis   389632256 conflicts 15199512449948 propagations       70 conflicts/sec  2743256 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129927 |  320571731 |  193994943 |  1465788 |  1535493 |  8200671 |  8271934 |  4084203 | 29.515 |
c |  1 | 3175008 |  326322715 |  195637978 |  1471965 |  1434743 |  8271952 |  8200671 |  3980437 | 29.515 |
c 
c synthesis   389632921 conflicts 15199539844834 propagations       70 conflicts/sec  2743257 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129935 |  320572304 |  193995329 |  1465788 |  1535879 |  8200766 |  8272066 |  4084250 | 29.515 |
c |  1 | 3175015 |  326323236 |  195638355 |  1471965 |  1435120 |  8272093 |  8200759 |  3980477 | 29.515 |
c 
c synthesis   389633684 conflicts 15199567657274 propagations       70 conflicts/sec  2743258 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129942 |  320572794 |  193995660 |  1465788 |  1536210 |  8200865 |  8272220 |  4084279 | 29.515 |
c |  1 | 3175022 |  326323668 |  195638687 |  1471965 |  1435452 |  8272229 |  8200865 |  3980508 | 29.515 |
c 
c synthesis   389634347 conflicts 15199594378070 propagations       70 conflicts/sec  2743259 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129947 |  320573150 |  193995924 |  1465788 |  1536474 |  8201011 |  8272339 |  4084303 | 29.515 |
c |  1 | 3175028 |  326324107 |  195638995 |  1471965 |  1435759 |  8272345 |  8201003 |  3980534 | 29.515 |
c 
c synthesis   389634919 conflicts 15199618598085 propagations       70 conflicts/sec  2743259 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129953 |  320573598 |  193996221 |  1465788 |  1536771 |  8201132 |  8272460 |  4084322 | 29.515 |
c |  1 | 3175035 |  326324591 |  195639345 |  1471966 |  1436110 |  8272470 |  8201131 |  3980554 | 29.515 |
c 
c synthesis   389635566 conflicts 15199645282047 propagations       70 conflicts/sec  2743260 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129959 |  320574053 |  193996549 |  1465788 |  1537099 |  8201298 |  8272560 |  4084358 | 29.515 |
c |  1 | 3175041 |  326325074 |  195639692 |  1471966 |  1436457 |  8272569 |  8201279 |  3980599 | 29.515 |
c 
c synthesis   389636241 conflicts 15199672836680 propagations       70 conflicts/sec  2743261 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129967 |  320574652 |  193996936 |  1465788 |  1537486 |  8201398 |  8272678 |  4084390 | 29.515 |
c |  1 | 3175048 |  326325555 |  195640012 |  1471966 |  1436777 |  8272684 |  8201394 |  3980648 | 29.515 |
c 
c synthesis   389636948 conflicts 15199701151762 propagations       70 conflicts/sec  2743262 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129973 |  320575072 |  193997234 |  1465788 |  1537784 |  8201537 |  8272777 |  4084413 | 29.515 |
c |  1 | 3175055 |  326326088 |  195640371 |  1471966 |  1437136 |  8272782 |  8201536 |  3980675 | 29.515 |
c 
c synthesis   389637605 conflicts 15199729601281 propagations       70 conflicts/sec  2743264 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129979 |  320575506 |  193997530 |  1465788 |  1538080 |  8201655 |  8272919 |  4084453 | 29.515 |
c |  1 | 3175060 |  326326463 |  195640653 |  1471966 |  1437418 |  8272924 |  8201642 |  3980720 | 29.515 |
c 
c synthesis   389638183 conflicts 15199753662637 propagations       70 conflicts/sec  2743264 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129985 |  320575961 |  193997831 |  1465788 |  1538381 |  8201766 |  8273065 |  4084497 | 29.515 |
c |  1 | 3175067 |  326326937 |  195641008 |  1471966 |  1437773 |  8273065 |  8201746 |  3980753 | 29.515 |
c 
c synthesis   389638839 conflicts 15199779928778 propagations       70 conflicts/sec  2743265 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129990 |  320576429 |  193998146 |  1465788 |  1538696 |  8201895 |  8273198 |  4084553 | 29.515 |
c |  1 | 3175073 |  326327327 |  195641306 |  1471966 |  1438071 |  8273237 |  8201876 |  3980793 | 29.515 |
c 
c synthesis   389639452 conflicts 15199802953450 propagations       70 conflicts/sec  2743265 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3129997 |  320576935 |  193998499 |  1465788 |  1539049 |  8202016 |  8273318 |  4084587 | 29.515 |
c |  1 | 3175080 |  326327846 |  195641672 |  1471966 |  1438437 |  8273335 |  8202003 |  3980834 | 29.515 |
c 
c synthesis   389640171 conflicts 15199831357134 propagations       70 conflicts/sec  2743266 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130003 |  320577379 |  193998820 |  1465788 |  1539370 |  8202149 |  8273451 |  4084629 | 29.515 |
c |  1 | 3175087 |  326328332 |  195642034 |  1471966 |  1438799 |  8273476 |  8202128 |  3980874 | 29.515 |
c 
c synthesis   389640854 conflicts 15199858279414 propagations       70 conflicts/sec  2743267 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130010 |  320577875 |  193999170 |  1465788 |  1539720 |  8202274 |  8273612 |  4084670 | 29.515 |
c |  1 | 3175095 |  326328887 |  195642427 |  1471966 |  1439192 |  8273637 |  8202258 |  3980910 | 29.515 |
c 
c synthesis   389641597 conflicts 15199888325324 propagations       70 conflicts/sec  2743269 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130018 |  320578397 |  193999533 |  1465788 |  1540083 |  8202398 |  8273751 |  4084711 | 29.515 |
c |  1 | 3175102 |  326329425 |  195642785 |  1471966 |  1439550 |  8273752 |  8202390 |  3980960 | 29.515 |
c 
c synthesis   389642318 conflicts 15199918138163 propagations       70 conflicts/sec  2743270 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130023 |  320578766 |  193999796 |  1465788 |  1540346 |  8202522 |  8273864 |  4084738 | 29.515 |
c |  1 | 3175109 |  326329924 |  195643149 |  1471966 |  1439914 |  8273874 |  8202508 |  3981006 | 29.515 |
c 
c synthesis   389642945 conflicts 15199943237466 propagations       70 conflicts/sec  2743271 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130030 |  320579313 |  194000153 |  1465788 |  1540703 |  8202610 |  8273971 |  4084770 | 29.515 |
c |  1 | 3175116 |  326330426 |  195643494 |  1471966 |  1440259 |  8273978 |  8202608 |  3981048 | 29.515 |
c 
c synthesis   389643647 conflicts 15199971702548 propagations       70 conflicts/sec  2743272 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130037 |  320579876 |  194000543 |  1465788 |  1541093 |  8202702 |  8274055 |  4084808 | 29.515 |
c |  1 | 3175122 |  326330861 |  195643807 |  1471966 |  1440572 |  8274070 |  8202690 |  3981089 | 29.515 |
c 
c synthesis   389644350 conflicts 15200000182878 propagations       70 conflicts/sec  2743273 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130044 |  320580372 |  194000882 |  1465788 |  1541432 |  8202806 |  8274164 |  4084832 | 29.515 |
c |  1 | 3175129 |  326331381 |  195644166 |  1471966 |  1440931 |  8274172 |  8202791 |  3981127 | 29.515 |
c 
c synthesis   389645048 conflicts 15200029712200 propagations       70 conflicts/sec  2743274 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130051 |  320580879 |  194001221 |  1465788 |  1541771 |  8202916 |  8274276 |  4084863 | 29.515 |
c |  1 | 3175136 |  326331871 |  195644513 |  1471966 |  1441278 |  8274298 |  8202913 |  3981158 | 29.515 |
c 
c synthesis   389645734 conflicts 15200057985402 propagations       70 conflicts/sec  2743276 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130058 |  320581403 |  194001567 |  1465788 |  1542117 |  8203030 |  8274428 |  4084909 | 29.515 |
c |  1 | 3175143 |  326332337 |  195644852 |  1471966 |  1441617 |  8274428 |  8203028 |  3981182 | 29.515 |
c 
c synthesis   389646419 conflicts 15200087168684 propagations       70 conflicts/sec  2743277 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130065 |  320581905 |  194001936 |  1465788 |  1542486 |  8203168 |  8274525 |  4084940 | 29.515 |
c |  1 | 3175149 |  326332814 |  195645193 |  1471966 |  1441958 |  8274529 |  8203123 |  3981206 | 29.515 |
c 
c synthesis   389647129 conflicts 15200116931573 propagations       70 conflicts/sec  2743278 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130073 |  320582482 |  194002330 |  1465788 |  1542880 |  8203320 |  8274685 |  4084984 | 29.515 |
c |  1 | 3175157 |  326333354 |  195645578 |  1471970 |  1442343 |  8274686 |  8203304 |  3981254 | 29.515 |
c 
c synthesis   389647908 conflicts 15200148699246 propagations       70 conflicts/sec  2743280 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130080 |  320583006 |  194002728 |  1465788 |  1543278 |  8203502 |  8274795 |  4085029 | 29.515 |
c |  1 | 3175164 |  326333825 |  195645919 |  1471970 |  1442684 |  8274811 |  8203498 |  3981287 | 29.515 |
c 
c synthesis   389648647 conflicts 15200176540351 propagations       70 conflicts/sec  2743281 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130088 |  320583540 |  194003091 |  1465788 |  1543641 |  8203649 |  8274923 |  4085078 | 29.515 |
c |  1 | 3175170 |  326334294 |  195646227 |  1471970 |  1442992 |  8274924 |  8203645 |  3981324 | 29.515 |
c 
c synthesis   389649318 conflicts 15200204260071 propagations       70 conflicts/sec  2743282 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130095 |  320584058 |  194003466 |  1465788 |  1544016 |  8203778 |  8275051 |  4085109 | 29.515 |
c |  1 | 3175177 |  326334810 |  195646606 |  1471970 |  1443371 |  8275056 |  8203765 |  3981349 | 29.515 |
c 
c synthesis   389650072 conflicts 15200234384476 propagations       70 conflicts/sec  2743284 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130102 |  320584519 |  194003803 |  1465788 |  1544353 |  8203875 |  8275143 |  4085139 | 29.515 |
c |  1 | 3175185 |  326335425 |  195647002 |  1471970 |  1443767 |  8275151 |  8203871 |  3981373 | 29.515 |
c 
c synthesis   389650805 conflicts 15200265213821 propagations       70 conflicts/sec  2743285 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130108 |  320584945 |  194004116 |  1465788 |  1544666 |  8203998 |  8275256 |  4085161 | 29.515 |
c |  1 | 3175192 |  326335927 |  195647370 |  1471970 |  1444135 |  8275264 |  8203986 |  3981418 | 29.515 |
c 
c synthesis   389651486 conflicts 15200293041148 propagations       70 conflicts/sec  2743286 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130114 |  320585374 |  194004427 |  1465788 |  1544977 |  8204125 |  8275349 |  4085200 | 29.515 |
c |  1 | 3175200 |  326336490 |  195647747 |  1471970 |  1444512 |  8275358 |  8204124 |  3981449 | 29.515 |
c 
c synthesis   389652174 conflicts 15200322774883 propagations       70 conflicts/sec  2743288 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130123 |  320586017 |  194004859 |  1465788 |  1545409 |  8204237 |  8275484 |  4085238 | 29.515 |
c |  1 | 3175207 |  326337001 |  195648108 |  1471971 |  1444873 |  8275484 |  8204236 |  3981484 | 29.515 |
c 
c synthesis   389652967 conflicts 15200353778503 propagations       70 conflicts/sec  2743290 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130130 |  320586515 |  194005218 |  1465788 |  1545768 |  8204371 |  8275604 |  4085277 | 29.515 |
c |  1 | 3175213 |  326337441 |  195648426 |  1471971 |  1445191 |  8275604 |  8204361 |  3981533 | 29.515 |
c 
c synthesis   389653644 conflicts 15200383690103 propagations       70 conflicts/sec  2743291 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130137 |  320587018 |  194005583 |  1465788 |  1546133 |  8204524 |  8275713 |  4085300 | 29.515 |
c |  1 | 3175220 |  326337969 |  195648788 |  1471973 |  1445553 |  8275717 |  8204512 |  3981564 | 29.515 |
c 
c synthesis   389654371 conflicts 15200412881705 propagations       70 conflicts/sec  2743292 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130144 |  320587484 |  194005926 |  1465788 |  1546476 |  8204673 |  8275835 |  4085332 | 29.515 |
c |  1 | 3175226 |  326338343 |  195649067 |  1471973 |  1445832 |  8275835 |  8204671 |  3981603 | 29.515 |
c 
c synthesis   389654993 conflicts 15200439450563 propagations       70 conflicts/sec  2743293 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130150 |  320587903 |  194006242 |  1465788 |  1546792 |  8204814 |  8275930 |  4085370 | 29.515 |
c |  1 | 3175233 |  326338913 |  195649455 |  1471973 |  1446220 |  8275938 |  8204797 |  3981642 | 29.515 |
c 
c synthesis   389655697 conflicts 15200466943397 propagations       70 conflicts/sec  2743294 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130157 |  320588436 |  194006633 |  1465788 |  1547183 |  8204973 |  8276042 |  4085408 | 29.515 |
c |  1 | 3175240 |  326339419 |  195649781 |  1471973 |  1446546 |  8276048 |  8204968 |  3981673 | 29.515 |
c 
c synthesis   389656414 conflicts 15200496940826 propagations       70 conflicts/sec  2743296 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130164 |  320588844 |  194006944 |  1465788 |  1547494 |  8205117 |  8276186 |  4085443 | 29.515 |
c |  1 | 3175247 |  326339939 |  195650169 |  1471973 |  1446934 |  8276186 |  8205105 |  3981729 | 29.515 |
c 
c synthesis   389657113 conflicts 15200522953237 propagations       70 conflicts/sec  2743296 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130171 |  320589360 |  194007329 |  1465788 |  1547879 |  8205267 |  8276337 |  4085484 | 29.515 |
c |  1 | 3175255 |  326340490 |  195650573 |  1471973 |  1447338 |  8276346 |  8205264 |  3981792 | 29.515 |
c 
c synthesis   389657902 conflicts 15200551516770 propagations       70 conflicts/sec  2743298 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130178 |  320589868 |  194007700 |  1465788 |  1548250 |  8205422 |  8276449 |  4085512 | 29.515 |
c |  1 | 3175262 |  326340993 |  195650932 |  1471975 |  1447697 |  8276467 |  8205413 |  3981836 | 29.515 |
c 
c synthesis   389658632 conflicts 15200580343291 propagations       70 conflicts/sec  2743299 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130185 |  320590347 |  194008048 |  1465788 |  1548598 |  8205552 |  8276607 |  4085546 | 29.515 |
c |  1 | 3175270 |  326341505 |  195651314 |  1471975 |  1448078 |  8276625 |  8205551 |  3981880 | 29.515 |
c 
c synthesis   389659362 conflicts 15200608893287 propagations       70 conflicts/sec  2743300 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130193 |  320590899 |  194008435 |  1465788 |  1548985 |  8205656 |  8276789 |  4085569 | 29.515 |
c |  1 | 3175278 |  326342070 |  195651714 |  1471975 |  1448479 |  8276789 |  8205651 |  3981910 | 29.515 |
c 
c synthesis   389660149 conflicts 15200641411334 propagations       70 conflicts/sec  2743302 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130201 |  320591447 |  194008839 |  1465788 |  1549389 |  8205803 |  8276905 |  4085607 | 29.515 |
c |  1 | 3175285 |  326342608 |  195652096 |  1471975 |  1448861 |  8276907 |  8205785 |  3981947 | 29.515 |
c 
c synthesis   389660935 conflicts 15200672429586 propagations       70 conflicts/sec  2743304 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130209 |  320592012 |  194009269 |  1465788 |  1549819 |  8205964 |  8277066 |  4085659 | 29.515 |
c |  1 | 3175293 |  326343151 |  195652496 |  1471975 |  1449261 |  8277075 |  8205959 |  3981995 | 29.515 |
c 
c synthesis   389661765 conflicts 15200703176910 propagations       70 conflicts/sec  2743305 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130217 |  320592576 |  194009681 |  1465788 |  1550231 |  8206125 |  8277186 |  4085707 | 29.515 |
c |  1 | 3175300 |  326343646 |  195652853 |  1471975 |  1449618 |  8277200 |  8206118 |  3982056 | 29.515 |
c 
c synthesis   389662534 conflicts 15200731416341 propagations       70 conflicts/sec  2743306 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130224 |  320593012 |  194010014 |  1465788 |  1550564 |  8206297 |  8277370 |  4085743 | 29.515 |
c |  1 | 3175308 |  326344206 |  195653250 |  1471975 |  1450014 |  8277381 |  8206294 |  3982116 | 29.515 |
c 
c synthesis   389663264 conflicts 15200760546052 propagations       70 conflicts/sec  2743308 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130230 |  320593510 |  194010354 |  1465788 |  1550904 |  8206413 |  8277500 |  4085786 | 29.515 |
c |  1 | 3175315 |  326344739 |  195653624 |  1471975 |  1450389 |  8277521 |  8206406 |  3982156 | 29.515 |
c 
c synthesis   389663978 conflicts 15200790428603 propagations       70 conflicts/sec  2743309 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130237 |  320593958 |  194010684 |  1465788 |  1551234 |  8206550 |  8277687 |  4085830 | 29.515 |
c |  1 | 3175322 |  326345277 |  195653996 |  1471975 |  1450761 |  8277699 |  8206515 |  3982204 | 29.515 |
c 
c synthesis   389664680 conflicts 15200819690526 propagations       70 conflicts/sec  2743311 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130245 |  320594496 |  194011073 |  1465788 |  1551623 |  8206767 |  8277882 |  4085887 | 29.515 |
c |  1 | 3175330 |  326345780 |  195654384 |  1471975 |  1451149 |  8277889 |  8206750 |  3982264 | 29.515 |
c 
c synthesis   389665457 conflicts 15200849427369 propagations       70 conflicts/sec  2743312 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130251 |  320594900 |  194011382 |  1465788 |  1551932 |  8206918 |  8278066 |  4085926 | 29.515 |
c |  1 | 3175338 |  326346307 |  195654784 |  1471975 |  1451549 |  8278072 |  8206913 |  3982324 | 29.515 |
c 
c synthesis   389666166 conflicts 15200876617939 propagations       70 conflicts/sec  2743313 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130258 |  320595429 |  194011773 |  1465788 |  1552323 |  8207072 |  8278302 |  4085983 | 29.515 |
c |  1 | 3175346 |  326346834 |  195655208 |  1471975 |  1451973 |  8278332 |  8207059 |  3982370 | 29.515 |
c 
c synthesis   389666981 conflicts 15200906870469 propagations       70 conflicts/sec  2743314 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130266 |  320595995 |  194012177 |  1465788 |  1552727 |  8207234 |  8278470 |  4086041 | 29.515 |
c |  1 | 3175353 |  326347333 |  195655563 |  1471975 |  1452328 |  8278485 |  8207219 |  3982408 | 29.515 |
c 
c synthesis   389667740 conflicts 15200937938159 propagations       70 conflicts/sec  2743316 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130273 |  320596426 |  194012512 |  1465788 |  1180280 |  8207418 |  8278645 |  4086084 | 30.434 |
c |  1 | 3175361 |  326347840 |  195655937 |  1471975 |  1452702 |  8278649 |  8207418 |  3982459 | 30.434 |
c 
c synthesis   389668449 conflicts 15200967022168 propagations       70 conflicts/sec  2743317 propagations/sec
c Total Memory so far : 2840.29Mb
c
c |-------------------------------------------------------------------------------------------------------|
c | id | starts | decisions  |  confls    |  Init T  |  learnts | exported | imported | promoted |    %   | 
c |-------------------------------------------------------------------------------------------------------|
c |  0 | 3130280 |  320596902 |  194012893 |  1465788 |  1180660 |  8207593 |  8278797 |  4086136 | 32.176 |
c |  1 | 3175368 |  326348333 |  195656295 |  1471975 |  1105051 |  8278821 |  8207588 |  3982512 | 32.176 |
c 
c synthesis   389669188 conflicts 15200996679100 propagations       70 conflicts/sec  2743319 propagations/sec
c Total Memory so far : 2840.29Mb
c Thread 0 is 100% pure glucose! First thread to finish! (UNSAT answer).
c Total Memory so far : 2840.29Mb
c
c real time : 2.78326e+06 s
c cpu time  : 5.5411e+06 s
c
c
c
c |---------------------------------------- FINAL STATS --------------------------------------------------|
c
c |---------------|-----------------|------------|------------|
c | Threads       |      Total      |          0 |          1 |
c |---------------|-----------------|------------|------------|
c | Conflicts     |       389669523 |  194013055 |  195656468 |
c | Decisions     |       646945672 |  320597124 |  326348548 |
c | Propagations  |  15201010073323 | 7587336527673 | 7613673545650 |
c | Avg_Trail     |                 |     561547 |     564104 |
c | Avg_DL        |                 |         27 |         27 |
c | Avg_Res       |                 |          0 |          0 |
c | Avg_Res_Seen  |                 |          0 |          0 |
c |---------------|-----------------|------------|------------|
c | Exported      |        16486580 |    8207673 |    8278907 |
c | Imported      |        16486534 |    8278907 |    8207627 |
c | Good          |              27 |         14 |         13 |
c | Purge         |        16486507 |    8278893 |    8207614 |
c | Promoted      |         8068697 |    4086160 |    3982537 |
c | Remove_Imp    |        11551446 |    5837191 |    5714255 |
c | Blocked_Reuse |               0 |          0 |          0 |
c |---------------|-----------------|------------|------------|
c | Unaries       |                 |         10 |          3 |
c | Binaries      |                 |         39 |         14 |
c | Glues         |                 |         57 |         25 |
c |---------------|-----------------|------------|------------|
c | Orig_Seen     |            76 % |    1465788 |    1471975 |
c | Diff Orig seen|                 |      X     |       6187 |
c | Hamming       |             0 % |      X     |        334 |
c |---------------|-----------------|------------|------------|

s UNSATISFIABLE
