Source of the scripts used in the MathCheck2 system, as described in the following papers:

* MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (CASC 2016)
* Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures (JAR 2017)
* A SAT+CAS Method for Enumerating Williamson Matrices of Even Order (AAAI 2018)
* Enumeration of Complex Golay Pairs via Programmatic SAT (ISSAC 2018)
* A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples (AAAI 2019)
* SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics (CASCON 2019)
* The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices (AMAI 2019)
* Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture (JSC 2020)
* A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords (AAECC 2020)
* Nonexistence Certificates for Ovals in a Projective Plane of Order Ten (IWOCA 2020)
* Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem (IJCAI 2020)
* Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT (JSC 2021)
* A SAT-based Resolution of Lam's Problem (AAAI 2021)
* When Satisfiability Solving Meets Symbolic Computation (CACM 2022)