\begin{center}
\begin{tabular}{|l|r|r|r|r|r|r|}
  \hline         
  {\bf Experiment}&{\bf Front}&{\bf Fill}&{\bf Split}&{\bf Rec}&{\bf Total}\\
  \hline
  Cartesian Closed Categories&0.058&1.000&0.004&0.036&1.099\\
  \hline
  CPM Completeness&0.900&0.916&0.010&0.117&1.134\\
  CPM Proof equivalence: $\Arrow$ &0.249&0.226&0.034&0.442&0.951\\
  CPM Proof equivalence: $\Leftarrow$ &0.274&0.280&0.033&0.647&1.235\\
  \hline
  Horn LP Soundness&0.112&4.336&0.004&0.049&4.501\\
  Horn LP Canonical forms&0.159&0.028&0.009&0.107&0.303\\
  Horn LP Completeness&0.137&0.015&0.005&0.039&0.195\\
  \hline
  Mini-ML Value soundness &0.055&0.016&0.041&0.061&0.172\\
  Mini-ML Type preservation&0.066&0.062&0.521&0.150&0.799\\
  Mini-ML Evaluation/Reduction&0.064&25.397&0.007&0.078&25.546\\
  \hline
  Hilbert's abstraction theorem&0.111&0.197&0.004&0.010&0.322\\
  \hline
  Associativity of $+$&0.026&0.009&0.012&0.016&0.063\\
  Commutativity of $+$&0.037&0.092&0.609&4.139&4.877  \\
\hline
\end{tabular}
\end{center}
\medskip
\begin{description}
\item Timings in secs. 
\item Hardware: Pentium II (300 Mhz)
\item Software: Linux 2.30, NJ-SML 1.10, Twelf 1.2
\end{description}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 
