\section{Results (old - remove!)}

\todo{the following list can be removed. 
  Evaluation and numerical data will be give for each cat. separately.
}



for each categories, 
list all participating tools, 
and some overview data: best, average, total
for number, time, proof size of yes and no.

(to get these numbers, will apply the Query interface,
which is under development in Leipzig)

Participants:
\begin{verbatim}
http://lists.lri.fr/pipermail/termtools/2008-November/000633.html

final list of registrations:
AProVE			FP Category
				LP Category
				SRS Standard
				TRS Contextsensitive
				TRS Innermost
				TRS Standard
				TRS Termination modulo Theory
AProVE-A3PAT	SRS Standard Certifying
				TRS Standard Certifying
AProVE-CERT	SRS Standard Certifying
				TRS Standard Certifying
AProVE-COLOR	SRS Standard Certifying
				TRS Standard Certifying
CaT				Derivational Complexity - Full Rewriting
				Derivational Complexity - Innermost Rewriting
cime3			SRS Standard Certifying
				TRS Standard Certifying
Jambox			SRS Relative
				SRS Standard
				TRS Relative
				TRS Standard
matchbox		SRS Standard Certifying
				TRS Standard Certifying
nonloop			SRS Standard
polytool			LP Category
TCT-DC			Derivational Complexity - Full Rewriting
TCT-IDC		Derivational Complexity - Innermost Rewriting
TCT-IRC		Runtime Complexity Ã¢ÂÂ Innermost Rewriting
TCT-RC			Runtime Complexity Ã¢ÂÂ Full Rewriting
TTT2			SRS Standard
				TRS Standard
\end{verbatim}

Order:
\begin{verbatim}
http://lists.lri.fr/pipermail/termtools/2008-November/000633.html

Derivational Complexity - Full Rewriting
Derivational Complexity - Innermost Rewriting
FP Category
LP Category
Runtime Complexity Ã¢ÂÂ Full Rewriting
Runtime Complexity Ã¢ÂÂ Innermost Rewriting
SRS Relative
SRS Standard
SRS Standard Certifying
TRS Contextsensitive
TRS Innermost
TRS Relative
TRS Standard
TRS Standard Certifying
TRS Termination modulo Theory

Timeout for proving is 60 seconds, timeout for certification is 60  
seconds.
\end{verbatim}

New Problems:
\begin{verbatim}
http://lists.lri.fr/pipermail/termtools/2008-November/000633.html

New problems were submitted by:
	Carsten Fuhs (10 TRS, 2 TRS CSR)
	Peter Schneider-Kamp (10 LP)
	Martin Oppelt (8 SRS)
	JÃÂ¶rg Endrullis (17 TRS CSR)


\end{verbatim}

Results SRS-standard:
\begin{verbatim}
http://lists.lri.fr/pipermail/termtools/2008-November/000646.html

SRS-standard is finished, with TTT2 getting
slightly more YES than Aprove, and Jambox about half
(this may be related to TTT2 and Aprove using arctic matrices).

For non-termination, nonloop has twice the NOs of TTT2,
and TTT2 has twice the NOs of Aprove. (And nonloop solved
SRS/Zantema/z073, which was the whole point of the exercise.)
\end{verbatim}

