State clearly _which_ Hilbert system this tool uses

[xamidi]

Your README.md states

[L1], [L2], [L3] are three axioms proposed by Jan Łukasiewicz.

but Łukasiewicz found several systems with three axioms, e.g. there are three such systems in On Axiom Systems of Propositional Calculi. I (1965) alone, namely

• L₁: (CCpqCCqrCpr,CCNppp,CpCNpq),
• L₂: (CCCpqrCNpr,CCCpqrCqr,CCNprCCqrCCpqr), and
• L₃: (CpCqp,CCpCqrCCpqCpr,CCNpNqCqp).

Your tool uses L₃, as I figured out by looking at the code.
For instance, I called this system

Frege's calculus simplified by Łukasiewicz (CpCqp,CCpCqrCCpqCpr,CCNpNqCqp)

for historical reasons.

Some tools, such as mine (pmGenerator), can use different user-definable Hilbert systems, e.g. I exemplary illustrated the seven minimal 1-bases over classical {→,¬} connectives. Furthermore, Hilbert systems are not limited to classical propositional logic.
Thus I find it of crucial interest which Hilbert system(s) a tool is about. I would state this very visibly.

 
By looking at forks, I noticed your tool was earlier named WangProver, with description:

An Automatic Theorem Prover for L(X) in Wang's Book (数理逻辑 第2版 汪芳庭) in Scala.

I assume the author didn't do a good job at describing both Hilbert systems in general and the origins of the particular Hilbert system for propositional logic that it uses. Even the English Wikipedia article mentions how Hilbert systems are often misrepresented in literature.

 
On another note, have you ever heard of Metamath's proof minimization challenge pmproofs.txt? It is based on the same axioms as your tool, and your README.md states that the tool would be

generating nearly-minimal proofs

That is quite the assertion. Maybe you can successfully shrink some of the proofs there (several of which are most likely not nearly-minimal)? 😉

Note that I also have a proof minimization challenge to derive the axioms you are using (among others) from minimal 1-bases.