Skeptik is a tool focused on compression of proofs, but it's also possible to generate proofs using it's infrastructure.
There is a new algorithm developed by ANU employees, called Conflict Resolution algorithm, which has no implementation yet and can generate proofs in first-order logic.
Conflict Resolution algorithm extends wellknown SAT solver DPLL and CDCL algorithm and tries to generalize it’s ideas for first-order logic. In CR we negate instances (substitutions) of decision literals (unlike CDCL where we negate decision literals), but main idea is the same: we decide to assign truthness to some atom and then try to propagate and achieve truthness of some other atoms. Eventually, we will reach a conflict or satisfactions and generate some conflict clauses if reached conflict.