This problem can be solved using Z3: https://gist.github.com/zb3/c59cf596ce80c501db5ca16c31a1c3a7

I don't know whether autor used solver or some other magic method... Solutions should be available to those who want to see them.