FOL_Refutation_Prover Refutation Prover for FOL using First-Order Resolution Unification algorithm FOL-to-CNF algorithm Resolution algorithm