\newchapter{Equations}

\leveldown{}

\input{equations/calc/main_EN}
\input{equations/xkcd287/main_EN}
\input{equations/kantorovich/main_EN}
\input{equations/animals/main_EN}
\input{equations/subset/main_EN}
\input{equations/2017_AMC_12A_Problem_2_EN}
\input{equations/modinv/main_EN}
\input{equations/KLEE_eq/main_EN}
\input{equations/CBMC_eq/main_EN}
\input{equations/minesweeper/main_EN}
\input{equations/LCG/main_EN}
\input{equations/factor_SMT/main_EN}
\input{equations/factor_SAT/main_EN}
\input{equations/spreadsheet/main_EN}
\input{equations/tomo/main_EN}
\input{equations/cribbage/main_EN}
\input{equations/pe31/main_EN}
\input{equations/TAOCP_7_1_3_exercise_15/main_EN}
\input{equations/de_bruijn_SMT/main_EN}
\input{equations/surd/main_EN}

\myheading{Exercise}

As an exercise, try to encode this problem using SMT-LIB 2.0 or Z3Py API:

\begin{framed}
\begin{quotation}
If a merchant buys 138 yards of cloth, some of which is black and some blue, for 540 roubles,
how many yards of each did he buy if the blue cloth cost 5 roubles a yard and the black cloth 3?
\end{quotation}
\end{framed}
( Anton Chekhov - The Tutor\footnote{\href{https://www.ibiblio.org/eldritch/ac/tutor.htm}{English translation},
\href{https://ilibrary.ru/text/1103/p.1/index.html}{Russian original}}. )

\levelup{}