REMIS: The Davenport-Heintz Example

Description of the problem on p.325: This formula is a special case of more general formula used by Davenport and Heintz in order to show the time complexity of the quantifier elimination in elementary algebra and geometry.

also in Loos & Weispfenning

davhei := ex(c,all({a,b},(a=d and b=c) or (a=c and b=1) impl a**2 = b));

end;  % of file