[freemint]

Quantified SAT is decidable. Are you aware of any theories where expressions with quantors over finitely many choices are unsatisfiable but quantor free expressions are satisfiable over the same theory?