  Quantifier elimination over the reals is a central problem in computational
real algebraic geometry, polynomial system solving and symbolic computation.
Given a semi-algebraic formula (whose atoms are polynomial constraints) with
quantifiers on some variables, it consists in computing a logically equivalent
formula involving only unquantified variables. When there is no alternate of
quantifier, one has a one block quantifier elimination problem.
  We design a new practically efficient algorithm for solving one block
quantifier elimination problems when the input semi-algebraic formula is a
system of polynomial equations satisfying some mild assumptions such as
transversality. When the input is generic, involves $s$ polynomials of degree
bounded by $D$ with $n$ quantified variables and $t$ unquantified ones, we
prove that this algorithm outputs semi-algebraic formulas of degree bounded by
$\mathcal{D}$ using $O\ {\widetilde{~}}\left (n\ 8^{t}\ \mathcal{D}^{3t+2}\
  \binom{t+\mathcal{D}}{t} \right )$ arithmetic operations in the ground field
where $\mathcal{D} = n\ D^s(D-1)^{n-s+1}\ \binom{n}{s}$.
  In practice, it allows us to solve quantifier elimination problems which are
out of reach of the state-of-the-art (up to $8$ variables).
