definitions.tex
\lstdefinelanguage{empty}{}
\newtheorem{thm}{Theorem}
\newtheorem{cor}{Corollary}
\newtheorem{lem}{Lemma}

\theoremstyle{definition}
\newtheorem{defi}{Definition}
\newtheorem{ex}{Example}
\newtheorem{rem}{Remark}

\newcommand{\CC}{\mathcal{C}}
\newcommand{\FF}{\mathcal{F}}
\newcommand{\GG}{\mathcal{G}}
\newcommand{\HH}{\mathcal{H}}
\newcommand{\OO}{\mathcal{O}}
\newcommand{\RR}{\mathcal{R}}
\newcommand{\TT}{\mathcal{T}}
\newcommand{\VV}{\mathcal{V}}

\newcommand{\lpo}{\succ_{\mathrm{lpo}}}
\newcommand{\qlpo}{\succsim_{\mathrm{lpo}}}
\newcommand{\elpo}{\sim_{\mathrm{lpo}}}
\renewcommand{\l}{\langle}
\renewcommand{\r}{\rangle}
\newcommand{\remb}{\trianglerighteq_{\mathrm{emb}}}
\newcommand{\premb}{\vartriangleright_{\mathrm{emb}}}
\newcommand{\lemb}{\trianglelefteq_{\mathrm{emb}}}
\newcommand{\plemb}{\vartriangleleft_{\mathrm{emb}}}
\newcommand{\T}{\mathsf{T}}
\newcommand{\F}{\mathsf{F}}
\renewcommand{\t}[1]{\texttt{#1}}
\renewcommand{\rm}[1]{\textrm{#1}}
\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\limplies}{\rightarrow}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\lex}{\succsim^{\mathrm{lex}}_{\mathrm{lpo}}}
\newcommand{\TTT}{\textsf{T\!\raisebox{-1mm}{T}\!T}}



cod_all.tex
\begin{table}[bp]
\begin{center}
%\begin{tabular}{|cc|}
%\hline
%strict LPO & quasi LPO \\
%\hline
%  7.89 & 10.26\\
%\hline
%\end{tabular}
\subtable[strict LPO]{
\begin{tabular}{|lcc|}
\hline
        & poSAT & \texttt{SAT}\\
\hline
Total   & 9.112 & 7.666 \\
Average & 0.012 & 0.010 \\
Max     & 0.450 & 0.449 \\
\hline
\end{tabular}
}
\qquad
\subtable[quasi LPO]{
\begin{tabular}{|l r@{.}l r@{.}l |}
\hline
        & \multicolumn{2}{c}{poSAT} & \multicolumn{2}{c|}{\texttt{SAT}}\\
\hline
Total   & 10&428 & 10&690 \\
Average & 0&014 & 0&014 \\
Max     & 1&169 & 0&532 \\
\hline
\end{tabular}
}
\caption{751 instances for poSAT versus 773 instances for \texttt{SAT}.}
\label{RES:cod_all}
\end{center}
\end{table}

cod_hard.tex

\begin{table}[t]
\renewcommand{\to}{\texttt{TO}}
\begin{center}
\begin{tabular}{|lcccc|}
\hline
TRS & \texttt{SAT} &\texttt{BDD2}& \texttt{BDD3} &\texttt{TTT} \\
\hline
  \sf{AProVE\_AAECC-ring          } & 0.117 &\to  & 0.081      &0.062 \\
  \sf{Cime\_mucrl1                } & 0.296 &0.298& 0.296      &0.932 \\
  \sf{HM\_t005                    } & 0.449 &0.447& 0.449      &\to   \\
  \sf{HM\_t009                    } & 0.123 &\to  & \to        &0.062 \\
  \sf{TRCSR\_Ex1\_2\_AEL03\_C     } & 0.150 &\to  & \it{0.332} &0.121  \\
  \sf{TRCSR\_Ex5\_7\_Luc97\_C     } & 0.117 &\to  & \to        &0.089  \\
  \sf{TRCSR\_Ex6\_15\_AEL02\_C    } & 0.233 &\to  & \it{8.134} &0.171 \\
  \sf{TRCSR\_Ex6\_15\_AEL02\_GM   } & 0.109 &\to  & \to        &0.038  \\
  \sf{TRCSR\_ExAppendixB\_AEL03\_C} & 0.172 &\to  & \it{0.572} &0.151  \\
  \sf{Zantema\_z30                } & 0.091 &0.091& 0.091      &\to   \\
 % TRCSR\_ExSec11\_1\_Luc02a\_C&(0.084)&\to  &\to         &0.075& 0.155 \\
\hline
\end{tabular}
\caption{The 10 hardest problems for the symbol based encoding.}
\label{RES:cod_hard}
\end{center}
\end{table}

master.bbl
\begin{thebibliography}{10}

\bibitem{AG-TCS00}
T.~Arts and J.~Giesl.
\newblock Termination of {T}erm {R}ewriting using {D}ependency {P}airs.
\newblock {\em Theoretical Computer Science}, 236:133--178, 2000.

\bibitem{COD05}
M.~Codish, V.~Lagoon, and P.~Stuckey.
\newblock {S}olving {P}artial {O}rder {C}onstraints for {LPO} {T}ermination.
\newblock Technical report, Available from \texttt{arxiv.org/abs/cs/0512067},
  2005.

\bibitem{MSAT}
N.~E\'en and N.~S\"orensson.
\newblock {M}ini{S}at,\\
  \texttt{www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat}.

\bibitem{HM-IC05}
N.~Hirokawa and A.~Middeldorp.
\newblock Automating the {D}ependency {P}air {M}ethod.
\newblock {\em Information and Computation}, 199(1,2):172--199, 2005.

\bibitem{TPDB}
773 instances of~the Termination Problem Data Base~(TPDB).
\newblock \texttt{www.lri.fr/\textasciitilde marche/tpdb}.

\bibitem{KK04}
M.~Kurihara and H.~Kondo.
\newblock Efficient {BDD} {E}ncodings for {P}artial {O}rder {C}onstraints with
  {A}pplications to {E}xpert {S}ystems in {S}oftware {V}erification, {P}roc. of
  the 17th {I}nternational {C}onference on {I}ndustrial and {E}ngineering
  {A}pplications of {A}rtificial {I}ntelligence and {E}xpert {S}ystems.
\newblock {\em {L}ecture {N}otes in {A}rtificial {I}ntelligence},
  3029:827--837, 2004.

\bibitem{OCaml-refman}
X.~Leroy, D.~Doligez, J.~R\'{e}my, and J.~Vouillon.
\newblock {\em The Objective Caml system release 3.09}.

\bibitem{MID05}
A.~Middeldorp.
\newblock {\em {T}erm {R}ewriting}.
\newblock Lecture Notes, University of Innsbruck, 2005.

\bibitem{SWIG}
SWIG.
\newblock \texttt{www.swig.org}.

\bibitem{TTT}
Tyrolean~Termination Tool.
\newblock \texttt{cl2-informatik.uibk.ac.at/ttt}.

\bibitem{TSE68}
G.~Tseitin.
\newblock {O}n the {C}omplexity of {D}erivation in {P}ropositional {C}alculus.
\newblock {\em {S}tudies in {C}onstructive {M}athematics and {M}athematical
  {L}ogic, {P}art 2}, pages 115--125, 1968.

\bibitem{WIL90}
J.~Wilson.
\newblock {C}ompact {N}ormal {F}orms in {P}ropositional {Logic} and {I}nteger
  {P}rogramming {F}ormulations.
\newblock {\em Computers and Operations Research}, 17(3):309--314, 1990.

\bibitem{ZAN06}
H.~Zankl.
\newblock {B}inary {D}ecision {D}iagrams for {L}exicographic {P}ath {O}rders.
  {S}eminar {R}eport, 2006.

\end{thebibliography}
