What kind of math problems can be solved by automated theorem provers?

Question

Can I prove following statements with using available automated theorem provers?

1. $(a+b)^2=a^2+b^2+2ab$.

2. If $ 11 \mid 2a-3b$, then $ 11 \mid 7a-5b $.

3. If $ ax^2+bx+c=0$, then $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$.

4. If $a$ is even then $4a$ is even.

and so on!

I am asking this question because I just found the application of Automated theorem provers in proving theorems in logic.