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