\subsection{SMT format solution}
The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a4.py}. The Python
-script optimizes a little bit from the original formula by leaving out the
-$i=j$ comparison in subformula 17 and 18 by removing them from the set looped
-over. The script also optimizes by not checking variables $a_0^n$ and $a_I^n$
-since they always stay the same anyways. The minimization is done by
+conversion and said script is listed in Listing~\ref{listing:a4.bash}. The
+Python script optimizes a little bit from the original formula by leaving out
+the $i=j$ comparison in subformula 17 and 18 by removing them from the set
+looped over. The script also optimizes by not checking variables $a_0^n$ and
+$a_I^n$ since they always stay the same anyways. The minimization is done by
incrementing variable $N$ every time the current $N$ yields unsat with a bash
script shown in Listing~\ref{listing:4.bash}.
-\lstinputlisting[language=bash,
+\lstinputlisting[language=bash,firstline=58,
caption={Iteratively find the shortest solution for problem 4},
label={listing:4.bash}]{src/a4.bash}
\subsection{Solution}
The bash script finds and shows the minimal solution in which the postcondition
-is satisfied for $N=11$. Finding this solution takes less then $75$ seconds and
+is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
is shown in Table~\ref{tab:s4}.
Every line in the table represents the iteration and the bold items represent