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