\documentstyle[12pt,supertab]{article}
\begin{document}
\tablefirsthead{\hline\multicolumn{5}{|c|}{DIMACS 1996 SAT
BENCHMARKS}\\\hline File&Code&Variables&Clauses&Satisfiable?\\\hline}
\tablehead{\hline\multicolumn{5}{|c|}{DIMACS SAT
BENCHMARKS (cont.)}\\\hline File&Code&Variables&Clauses&Satisfiable?\\\hline}
\tablelasttail{\hline}
\begin{supertabular}{|lc|rr|c|}
tm1-yes.cnf   &(TMap)   &2421 &40723  &Yes\\  
tm2-yes.cnf   &(TMap)   &337  &1888   &Yes\\
as1-yes.cnf   &(Async)  &1044 &35386  &Yes\\
as2-yes.cnf   &(Async)  &96   &954    &Yes\\
as3-yes.cnf   &(Async)  &96   &954    &Yes\\
as4-yes.cnf   &(Async)  &328  &4176   &Yes\\
as5-yes.cnf   &(Async)  &1208 &31124  &Yes\\
as6-yes.cnf   &(Async)  &184  &2277   &Yes\\
as7-yes.cnf   &(Async)  &760  &17896  &Yes\\
as8-yes.cnf   &(Async)  &84   &974    &Yes\\
as9-no.cnf    &(Async)  &108  &1346   &No \\
as10-yes.cnf  &(Async)  &216  &2780   &Yes\\
as11-yes.cnf  &(Async)  &112  &1312   &Yes\\
as12-yes.cnf  &(Async)  &72   &1012   &Yes\\
as13-yes.cnf  &(Async)  &232  &2276   &Yes\\
as14-yes.cnf  &(Async)  &92   &758    &Yes\\
as15-yes.cnf  &(Async)  &232  &3692   &Yes\\
\end{supertabular}

\bigskip
{\bf NOTES:}

\begin{description}

\item[Async] From Jun Gu {\tt jungu@dimacs.rutgers.edu} and
	          Ruchir Puri {\tt puri@watson.ibm.com}.
     Instances from Asynchronous Circuit Synthesis:
     designing asynhronous circuits from generalized 
     concurrent specifications.  

\item[TMap] From Jun Gu {\tt jungu@dimacs.rutgers.edu} and
	         Ruchir Puri {\tt puri@watson.ibm.com}. 
     Instances from Technology Mapping: 
     mapping the gate level circuit into an implementation
     using standard cell library. 

\end{description}

\end{document}



