UC Berkeley, ABC 1.01 (compiled Jan 20 2007 16:47:34)
abc.rc: No such file or directory
Loaded "abc.rc" from the parent directory.
abc 01> test
Found last conflict after adding unit clause number 10229!
Roots = 7184. Learned = 3047. Total = 10231. Steps = 196361.  Ave = 62.09.  Used = 2224. Ratio = 0.73.
Runtime stats:
Reading  =   0.03 sec
BCP      =   0.32 sec
Trace    =   0.06 sec
TOTAL    =   0.43 sec
abc 01> test
Found last conflict after adding unit clause number 7676!
Roots = 6605. Learned = 1073. Total = 7678. Steps = 52402.  Ave = 42.68.  Used = 1011. Ratio = 0.94.
Runtime stats:
Reading  =   0.01 sec
BCP      =   0.02 sec
Trace    =   0.02 sec
TOTAL    =   0.06 sec
abc 01> test
Found last conflict after adding unit clause number 37868!
Roots = 15443. Learned = 22427. Total = 37870. Steps = 2365472.  Ave = 104.79.  Used = 19763. Ratio = 0.88.
Runtime stats:
Reading  =   0.20 sec
BCP      =  14.67 sec
Trace    =   0.56 sec
TOTAL    =  15.74 sec
abc 01>


abc 05> wb ibm_bmc/len25u_renc.blif
abc 05> ps
(no name)    : i/o =  348/   1  lat =    0  nd =  3648  bdd  = 15522  lev = 246
abc 05> sat -v
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |   17413    54996 |    5804       0        0     0.0 |  0.000 % |
|       100 |   17413    54996 |    6384     100      606     6.1 |  0.417 % |
|       250 |   17413    54996 |    7023     250     1586     6.3 |  0.417 % |
|       476 |   17413    54996 |    7725     476     3288     6.9 |  0.417 % |
|       813 |   17413    54996 |    8498     813     7586     9.3 |  0.417 % |
|      1319 |   17403    54970 |    9347    1318    14848    11.3 |  0.442 % |
|      2078 |   17403    54970 |   10282    2076    40186    19.4 |  0.466 % |
|      3217 |   17397    54948 |   11310    3208    99402    31.0 |  0.466 % |
|      4926 |   17392    54930 |   12441    4911   131848    26.8 |  0.491 % |
|      7489 |   17392    54930 |   13686    7474   204217    27.3 |  0.491 % |
|     11336 |   17357    54829 |   15054   11310   332863    29.4 |  0.638 % |
|     17103 |   17346    54794 |   16559    9130   203029    22.2 |  0.687 % |
|     25752 |   17288    54606 |   18215    9083   176982    19.5 |  0.834 % |
|     38727 |   17266    54536 |   20037   12674   278949    22.0 |  0.883 % |
|     58188 |   17240    54453 |   22041   11905   255255    21.4 |  0.957 % |
==============================================================================
Start =   15. Conf =  79435. Dec = 130967. Prop = 24083434. Insp = 136774586.
Total runtime =   18.66 sec.  Var select =    0.00 sec.  Var update =    0.00 sec.
UNSATISFIABLE  Time =  18.69 sec
abc 05>
abc 05> test
Found last conflict after adding unit clause number 96902!
Roots = 17469. Learned = 79435. Total = 96904. Steps = 9700042.  Ave = 121.89.  Used = 57072. Ratio = 0.72.
Runtime stats:
Reading  =   1.26 sec
BCP      = 204.99 sec
Trace    =   2.85 sec
TOTAL    = 209.85 sec