Introduction In recent years Large Language Models (LLMs) have improved significantly in the ability to ingest massive amounts of information and produce statistically relevant answers to queries. Unfortunately there is a lack of formalism with this approach, and real reasoning is absent in LLM responses. Symbolic AI on the other hand is able to logically reason through a problem with concrete steps, but draw from a relatively small quantity of formal axioms, and are thus limited to specific domains. The neuro-symbolic approach draws from the benefits of both, and limits the disadvantages inherent in each. We present a system that can take natural language and translate sentences into higher order formal axioms using a LLM. Automated theorem proving (ATP) is then used to ensure our growing knowledge base is consistent, and to answer questions from our knowledge base in a provable way. Human language is expressive and diverse, more so than can be expressed in First Order Logic. Thus to create our system, we use a large ontology called Suggested Upper Merged Ontology (SUMO), which contains over 230,000 axioms formalized with expressive higher order logics. Axioms in SUMO are continuously being checked for consistency.