%&ar
\begin{document}
\maketitle
\tableofcontents

\section{Introduction}
Implementing all the problems by hand in SMT-Lib format would be too much work
and therefore all problems have an accompanying bash script that does the
generation and/or the mini or maximization. The bash scripts all have a
function defined called \lstinline{generate} with a parameter that will be used
for mini or maximization. All solving is done on the benchmark system listed in
Listing~\ref{listing:benchmark}.

\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
RAM: 8GB

Yices: 2.4.1
SMT-Lib: 1.2
Bash: 4.3.30(1)
\end{lstlisting}

\newpage
\input{1.tex}

\newpage
\input{2.tex}

\newpage
\input{3.tex}

\newpage
\input{4.tex}

\newpage
\input{a.tex}

\end{document}
