\subsection{Solution}
The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
\textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
-listed in Table~\ref{tab:sol}.
-
+listed in Table~\ref{tab:sol}. \textsc{z3} finds a solution in $10$ minutes and
+$37$ seconds.
\begin{table}[h]
\centering