Translating Thought: Advancing First-Order Logic Interpretation with Llama2 and Z3 Solver