Apr 2026 Enumerating Choice Terms in Model-Based Quantifier Instantiation Feb 2026 Tao's Equational Proof Challenge Accepted May 2025 Augmenting Model-Based Instantiation with Fast Enumeration in SMT