CNF Benchmark Suite: VLIW-UNSAT-3.0
========================================

Description:    unsatisfiable formulas from formal verification of VLIW processors with instruction queues

# of instances: 2

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
-------------------------------------------------------------------------------------------------
9dlx_vliw_at_b_iq8_I3_C24.cnf        63647928       132413    1437279     9496335    6.607162 
9dlx_vliw_at_b_iq8_I3_C24_D.cnf      63512385       132156    1436566     9476916    6.596923




output of md5sum:
-------------------------------------------------------------------------------------------------
8f0b8c709479fa92fd93bc5a016e49db  9dlx_vliw_at_b_iq8_I3_C24.cnf
fbbc4078768e0fe68be7d57eb62e1fe0  9dlx_vliw_at_b_iq8_I3_C24_D.cnf