406380581··on A SAT Attack on Tarski's High School Algebra ProblemThe lower bound had already been established in prior work: https://zenodo.org/records/18568303