\myheading{Exercise 9 from TAOCP ``7.1.1 Boolean Basics'', solving it using Z3}

\renewcommand{\CURPATH}{FOL/TAOCP_7_1_1_exercise_9}

Page 34 from fasc0b.ps or \url{http://www.cs.utsa.edu/~wagner/knuth/fasc0b.pdf}.

\begin{figure}[H]
\centering
\frame{\includegraphics[scale=0.6]{\CURPATH/fasc0b_page34.png}}
\caption{Page 34}
\end{figure}

For (a):

\lstinputlisting[style=customsmt]{\CURPATH/Knuth_a.smt}

For (b):

\lstinputlisting[style=customsmt]{\CURPATH/Knuth_b.smt}

For (c):

\lstinputlisting[style=customsmt]{\CURPATH/Knuth_c.smt}

Results:

\lstinputlisting[style=customsmt]{\CURPATH/results.txt}