Blasting w SMT Solver seems to work

[chadbrewbaker]

I was able to solve a lot of these by asking ChatGPT to translate to SMTLIB then blast with Microsoft Z3 binary upload to Code Interpreter.

https://github.com/chadbrewbaker/ChadGPT/tree/main/codeint_toolbox

GPT here: https://chat.openai.com/g/g-hBDutiLmw-chadgpt

"Write a python program that shells out and executes 'bash /mnt/data/chadgpt.sh"

That should symlink the z3 binary to the path, then:

"Formulate this problem in SMTLIB then write a Python program that shells out and executes it on the command line with the z3 utility."

Obliged if you added Z3 and CVC5 along with Python bindings to the core GPT image, or had a GPT setting that allows you to boot the GPT with the binaries already symlinked.

Alternatively - to save yourselves $$$ in Azure credits, roll a more stripped down https://copy.sh/v86 Ubuntu 20.04 VM that ChatGPT can call as an oracle in the browser.