CNF Benchmark Suite: LIVENESS-SAT.1.0
========================================
Description: satisfiable CNF formulas from formal verification of liveness
of dual-issue superscalar DLX processors
# of instances: 10
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
------------------------------------------------------------------------------------------------------------
2dlx_cc_ex_bp_f_bug1_liveness.cnf 55831152 171648 2614464 7528066 2.879392
2dlx_cc_ex_bp_f_bug2_liveness.cnf 66391816 196655 3068742 8843042 2.881651
2dlx_cc_ex_bp_f_bug3_liveness.cnf 78722583 224920 3596474 10372084 2.883959
2dlx_cc_ex_bp_f_bug4_liveness.cnf 93030189 256697 4205986 12139670 2.886284
2dlx_cc_ex_bp_f_bug5_liveness.cnf 109530177 292249 4906188 14172012 2.888599
2dlx_cc_ex_bp_f_bug6_liveness.cnf 128456797 331848 5706594 16497116 2.890887
2dlx_cc_ex_bp_f_bug7_liveness.cnf 150058806 375775 6617342 19144842 2.893132
2dlx_cc_ex_bp_f_bug8_liveness.cnf 174600908 424320 7649214 22146964 2.895325
2dlx_cc_ex_bp_f_bug9_liveness.cnf 202364254 477782 8813656 25537230 2.897462
2dlx_cc_ex_bp_f_bug10_liveness.cnf 233646943 536469 10122798 29351422 2.899536
output of md5sum:
--------------------------------------------------------------------------------------------
d3869b114bb0dff542e25f3614f7423d 2dlx_cc_ex_bp_f_bug1_liveness.cnf
119942c0c4fc9d71ad0dc631d9ca7ee8 2dlx_cc_ex_bp_f_bug2_liveness.cnf
3a0af1030ba5ab83e5ffb0bac3958b2d 2dlx_cc_ex_bp_f_bug3_liveness.cnf
a3e0b7a5a85eca10e2c4fc3b8e9dbe35 2dlx_cc_ex_bp_f_bug4_liveness.cnf
8c534c95f6cc272df0b4b3683c9240bf 2dlx_cc_ex_bp_f_bug5_liveness.cnf
ebe34b026b75d6f4d87b49970d55c844 2dlx_cc_ex_bp_f_bug6_liveness.cnf
c0539ad44a0d78491578774e67737cd4 2dlx_cc_ex_bp_f_bug7_liveness.cnf
2c571ab8caef9e7efcd1b605b98f3144 2dlx_cc_ex_bp_f_bug8_liveness.cnf
0523c9b605200827b552d4525ff98cb0 2dlx_cc_ex_bp_f_bug9_liveness.cnf
1f373e7b127727b9a1289da9c95112e1 2dlx_cc_ex_bp_f_bug10_liveness.cnf