Quantifiers make first-order logic more expressive than propositional logic, but they also make solving satisfiability problems more difficult. To solve these problems efficiently, many techniques have been developed to eliminate quantifiers from logic formulas: model-based quantifier instantiation, E-matching, Skolemization, destructive equality resolution, ... I propose a table-based instantiation method for quantifier elimination. It can be used to solve satisfiability problems for "guarded" formulas, i.e., formulas where the use of defined functions in the matrix of quantifications effectively restricts the relevant range of their variables to a finite set. I have implemented this method in a pre-processor for SMT solvers. This "grounder" leverages an embedded relational database (SQLite) to execute relational operations efficiently. While this grounder does not accelerate 2025 benchmarks of the SMT-LIB library, it does improve performance of SMT solvers on public benchmarks for SAT and ASP solvers. The grounder has applications in, e.g., solving graph problems.