Rating:
A series of linear equations. This solution uses Z3 Prover.
https://advancedpersistentjest.com/2017/11/27/writeups-future-grammarless-tuctf/
I don't remember