Write-up without using Z3.

Original writeup (https://duksctf.github.io/2020/04/19/PLaidCTF-reee.html).