Quantifier elimination works just for additive arithmetic. It does not eliminate quantifiers from formulas where variables are multiplied with other variables. This is why quantifier elimination does not produce a reduced formula for your problem.
Notice, however, that a formula Exists x . phi[x] is equi-satisfiable to a formula of the form phi[x], so it should not be required to put an existential quantifier on your formula. The nlsat strategy handles quantifier-free formulas over the reals with multiplication.