Many inequalities involving the functions ln, exp, sin, cos, etc., can be proved automatically by MetiTarski: a resolution theorem prover (Metis) modied to call a decision procedure (QEPCAD) for the theory of real closed elds. The decision procedure simplies clauses by deleting literals that are inconsistent with other algebraic facts, while deleting as redundant clauses that follow algebraically from other clauses. MetiTarski includes special code to simplify arithmetic expressions.