It is a well-known theorem of Tarski that (what is now called) Tarski's elementary Euclidean geometry is a decidable theory. This is a first-order theory, as opposed to Hilbert's second-order axiomatization of Euclidean geometry.
My (somewhat vague) question is whether Tarski's axiomatization encompasses (i.e., proves) "most" geometry statements of interest, at least, say, at the college level geometry courses, so that one could arguably state that "Tarski's result mechanizes questions in Euclidean geometry" in such a context. In other words, I would like to have a better idea of the scope of "elementary geometry" within general Euclidean geometry.
I would also be happy if you could give me examples (or categories) of geometric statements that lie outside of the scope of Tarski's axiomatization (i.e., they essentially need something like Hilbert's second-order system).