  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 alternation of
quantifiers, one has a one block quantifier elimination problem.
  This paper studies a variant of the one block quantifier elimination in which
we compute an almost equivalent formula of the input. We design a new
probabilistic efficient algorithm for solving this variant when the input is a
system of polynomial equations satisfying some regularity assumptions. 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-s+1)\ 8^{t}\ \mathcal{D}^{3t+2}
\binom{t+\mathcal{D}}{t} \right )$ arithmetic operations in the ground field
where $\mathcal{D} = 2(n+s)\ 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).
