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

\renewcommand{\CURPATH}{FOL/TAOCP_7_1_1_exercise_56}

Page 41 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_page41.png}}
\caption{Page 41}
\end{figure}

For exists/forall/forall:

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

All the rest: \url{\RepoURL/\CURPATH}.

Results:

\lstinputlisting{\CURPATH/1.sh}

\begin{lstlisting}
unsat
unsat
unsat
sat
unsat
unsat
sat
sat
\end{lstlisting}