\myheading{Puzzle with animals}

\begin{figure}[H]
\centering
\includegraphics[scale=0.55]{equations/animals/1.jpg}
\caption{Found this elsewhere}
\end{figure}

This puzzle\footnote{\url{https://www.bhavinionline.com/2014/10/whatsapp-picture-puzzle-find-weight-rabbit-cat-dog/}}
can be solved easily, even with my toy MK85 solver:

\lstinputlisting[style=customsmt]{equations/animals/animals.smt}

\lstinputlisting{equations/animals/animals.txt}

However, one can argue that problem like that can be easily solved with bruteforce.
I'll make it more realistic and harder.

Let's say, there are 4 objects, each has a mass measured in some \textit{units}, in milligrams or even micrograms.
Each object's mass is 64-bit value.

We can use a weighting scale to measure object's mass, but as it happens in the real world, the scale is not precise.
We use two type of scales: the first can measure object down to $10^3 \cdot unit$,
the second down to $10^4 \cdot unit$.

We do our measures and we set mass in some range: [xxxx...000 - xxxx...999] and [xxxx...0000 - xxxx...9990].

\lstinputlisting[style=customsmt]{equations/animals/1.smt}

Even my toy MK85 can solve this:

\lstinputlisting{equations/animals/1.txt}

Almost correct, considering the fact that scales are not precise to the last \textit{unit}.

This is the data I used for the example:

\lstinputlisting[caption=Wolfram Mathematica code]{equations/animals/math.txt}