CNF Benchmark Suite: LIVENESS-UNSAT.1.0
========================================

Description:    unsatisfiable CNF formulas from formal verification of liveness
                of single-issue pipelined and dual-issue superscalar DLX processors

# of instances: 12

Author:         Miroslav N. Velev (mvelev@ece.cmu.edu)
                http://www.ece.cmu.edu/~mvelev

Date:           August 24, 2003



CNF Formula                  Size [Bytes]    Variables    Clauses    Literals    Avg. Literals/Clause
---------------------------------------------------------------------------------------------------
1dlx_c_liveness.cnf               1096986         6128      65112      185222                2.844668
1dlx_c_bp_f_liveness.cnf          1839678         9474     107213      305431                2.848824
1dlx_c_ex_liveness.cnf            3714732        18274     202528      576568                2.846856
1dlx_c_ex_bp_f_liveness.cnf       6276691        24104     339857      977353                2.875777
2dlx_ca_liveness.cnf             44983729       115049    2148917     6240189                2.903876
2dlx_ca_bp_f_liveness.cnf        95164304       202253    4313014    12562188                2.912624
2dlx_ca_ex_liveness.cnf         171411556       318771    7410689    21638261                2.919872
2dlx_ca_ex_bp_f_liveness.cnf    202854089       421107    8754014    25470592                2.909590
2dlx_cc_liveness.cnf             44830138       122395    2149255     6228463                2.897964
2dlx_cc_bp_f_liveness.cnf       134794488       267364    6003507    17508535                2.916385
2dlx_cc_ex_liveness.cnf         184062814       352057    7935053    23152635                2.917767
2dlx_cc_ex_bp_f_liveness.cnf    268764518       600698   11589474    33627416                2.901548




output of md5sum:
--------------------------------------------------------------------------------------------
a975824fd6dcc5b6ff81efd39b2a3c10  1dlx_c_liveness.cnf
42db30c3f27466c0cef0b06e4a8368e5  1dlx_c_bp_f_liveness.cnf
10676e763c2a0e75df6fcb494edc4acd  1dlx_c_ex_liveness.cnf
81a3ea64110d7782edcf1963c88dc131  1dlx_c_ex_bp_f_liveness.cnf
383ff2ffd68c163ceb016dc69afc886e  2dlx_ca_liveness.cnf
6b84b157293305009d9d0ab9aa6be7e8  2dlx_ca_bp_f_liveness.cnf
dd3dbbfcc25bc89fad248ff143761e64  2dlx_ca_ex_liveness.cnf
e4ae639c30121d186c21fbe903bfd414  2dlx_ca_ex_bp_f_liveness.cnf
d6af1b8104ac0412dc2c849239777266  2dlx_cc_liveness.cnf
02ecc6f6976b7fc5a8ef6ef7d261270d  2dlx_cc_bp_f_liveness.cnf
dd47ffb50595541a8c238d0a8bdee6bc  2dlx_cc_ex_liveness.cnf
5aaeb43608e227d23bdf358ffb395987  2dlx_cc_ex_bp_f_liveness.cnf