  We prove near-optimal trade-offs for quantifier depth versus number of
variables in first-order logic by exhibiting pairs of $n$-element structures
that can be distinguished by a $k$-variable first-order sentence but where
every such sentence requires quantifier depth at least $n^{\Omega(k/\log k)}$.
Our trade-offs also apply to first-order counting logic, and by the known
connection to the $k$-dimensional Weisfeiler--Leman algorithm imply
near-optimal lower bounds on the number of refinement iterations.
  A key component in our proof is the hardness condensation technique recently
introduced by [Razborov '16] in the context of proof complexity. We apply this
method to reduce the domain size of relational structures while maintaining the
minimal quantifier depth to distinguish them in finite variable logics.
