Dec. 19, 2000 These benchmarks are unsatisfiable, with the exception of 7pipe_bug. No known SAT-checker can prove the unsatisfiability of 6pipe.cnf in less than 60 hours of CPU time on a 336MHz SUN4. 7pipe.cnf should be more challenging than 6pipe.cnf. Miroslav mvelev@ece.cmu.edu http://www.ece.cmu.edu/~mvelev/