\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.063&0.312&0.004&0.058&0.437\\
  \hline
  CPM Completeness&0.069&0.209&0.024&0.310&0.611\\
  CPM Proof equivalence: $\Arrow$ &0.224&0.058&0.063&0.609&0.953\\
  CPM Proof equivalence: $\Leftarrow$ &0.227&0.083&0.063&0.551&0.924\\
  \hline
  Horn LP Soundness&0.105&1.004&0.004&0.081&1.194\\
  Horn LP Canonical forms&0.120&0.015&0.010&0.194&0.337\\
  Horn LP Completeness&0.178&0.008&0.005&0.072&0.262\\
  \hline
  Mini-ML Value soundness &0.041&0.008&0.027&0.113&0.188\\
  Mini-ML Type preservation&0.049&0.033&0.523&0.233&0.837\\
  Mini-ML Evaluation/Reduction &0.065&1.778&0.007&0.102&1.952\\
  \hline
  Hilbert's abstraction theorem&0.059&0.080&0.004&0.023&0.166\\
  \hline
  Associativity of $+$&-&-&-&-&-\\
  Commutativity of $+$&0.037&0.078&0.604&12.608&13.327   \\
  \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: 


