This paper presents a method for automating physics exam grading by combining a computer algebra system, an SMT solver, and a term rewriting system. A large-scale language model (LLM) is used to remove errors from student answers and rewrite them in a machine-readable format. The accuracy of these answers is then assessed using automated theorem-proving techniques (SMT solving and a term rewriting system tailored to physics problems). The system is evaluated using over 1,500 real student answers from the 2023 Australian Physics Olympiad. In particular, a detailed description of the development of the term rewriting system and the establishment of its finality and confluence properties is provided.