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

Description:    unsatisfiable CNF formulas from formal verification of liveness
                of single-issue pipelined and dual-issue superscalar DLX processors;
                the formulas are generated after applying abstraction techniques

# of instances: 9

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_bp_u_f_liveness.cnf        1108020         6874      65479      185121                2.827181
1dlx_c_ex_d_liveness.cnf          3770491        16011     210685      604761                2.870451
1dlx_c_ex_bp_u_f_liveness.cnf     2873003        14628     161477      460215                2.850034
2dlx_ca_bp_u_f_liveness.cnf      42382363       121388    2001843     5787895                2.891283
2dlx_ca_ex_d_liveness.cnf       121119441       235853    5459971    15948743                2.921031
2dlx_ca_ex_bp_u_f_liveness.cnf   87640265       223527    3922017    11363517                2.897366
2dlx_cc_bp_u_f_liveness.cnf      51833099       144071    2411213     6974643                2.892587
2dlx_cc_ex_d_liveness.cnf       137047217       266476    6144987    17949457                2.920992  
2dlx_cc_ex_bp_u_f_liveness.cnf  101992628       258649    4520142    13095280                2.897095




output of md5sum:
--------------------------------------------------------------------------------------------
f050daa1729cf105d8680d226803472d  1dlx_c_bp_u_f_liveness.cnf
4c83169779c8eeb50700dc2d17ad3aa2  1dlx_c_ex_d_liveness.cnf
89afec654ca98b941bc8e8485341720f  1dlx_c_ex_bp_u_f_liveness.cnf
ffa358aa9b7ab75ce0ff757b6ebbe9cc  2dlx_ca_bp_u_f_liveness.cnf
63256e1c08ee7ada009624e17b0ddc36  2dlx_ca_ex_d_liveness.cnf
5f57631f2533a787ef776851fc097332  2dlx_ca_ex_bp_u_f_liveness.cnf
63d1f77a8ace8aef27be33af53db3e37  2dlx_cc_bp_u_f_liveness.cnf
108a97d38b22ef9e31b44a5e67534096  2dlx_cc_ex_d_liveness.cnf
d680b783f94300cfd43ec2163e525daf  2dlx_cc_ex_bp_u_f_liveness.cnf