Sorry if any of this is unclear, or doesn't make much sense, I'm still trying to figure it out, a practical example such as this would likely help me understand better than anything else. I have read some articles about Tarski's proof of quantifier elimination for the reals, and I'm almost at the point of understanding the idea, although I'm still unclear how the algorithm works in practice, as in every source I found there were no examples. The basic idea of the algorithm was to use Sturm's ideas about counting roots, and creating lists of roots, and evaluating the signs on intervals of the real line.
For example, if I had the following statement
$\exists x. (ax^2 + bx + c > 0 \land dx + e > 0)$
According to one of the reference books I was looking at, putting this in quantifier free form involves listing the roots, i.e. if $p(x) = ax^2 + bx + c$ and $q(x) = dx + e$ then we could say e.g. $p(x)$ has roots $p_1, p_2$, where $p_1 < p_2$ and $q(x)$ has root $q_1$. There are three possible orderings assuming the roots are all distinct:
$p_1 < q_1 < p_2$
$p_1 < p_2 < q_1$
$q_1 < p_1 < p_2$
For each case, we can determine the truth of our original statement by evaluating the sign of $p(x)$ and $q(x)$ on the relevant intervals, e.g. in the first case,we evaluate the sign of $p(x)$ and $q(x)$ on the intervals $(-\infty, p_1), (p_1, q_1), (q_1, p_2), (p_2, \infty)$. I can see the relevance of this, but I don't really understand how this practically works to generate a quantifier free formula. Can anyone show how the algorithm actually would run in an example such as the one given? Even if someone could give an example of how the algorithm would run on a simpler example, such as $\exists x. ax^2 +bx + c > 0$, that would be helpful, as I can't really find any good worked examples. (Preferably not using CAD as I have no experience of it).