Hx is an incomplete axiomatic system in propositional logic. There are 145 formulas in data set.pdf, they are all tautologies (always being true). 115 (actually 114) of them are provable in Hx; 30 of them are unprovable in Hx. For any formula φ provable in Hx, there is a proof of φ; for any formula φ unprovable in Hx, it will be proved that φ is unprovable in Hx. Based on these formulas, by substitution, it's very easy to obtain millions of formulas provable in Hx, millions of formulas unprovable in Hx, millions of tautologies, and millions of contradictions (always being false).
For example:
p->p is provable in Hx and a tautology (see Proposition 22).
So, by substitution( p->(q->~r)/p ),
(p->(q->~r))->(p->(q->~r)) is also provable in Hx and a tautology. It will be guaranteed by a Theorem.
Moreover, by substitution( a/p,b/q,c/r ),
(a->(b->~c))->(a->(b->~c)) is also provable in Hx and a tautology.
A263=26*25*24=15600, 114*15600=1,778,400, so millions of formulas can be generated very quickly in this way.
((p->q)->p)->p (the Peirce' law) is unprovable in Hx itself (see Proposition 160), but ~~(((p->q)->p)->p) (the double negation of Peirce' law) is provable in Hx (see Proposition 159).
Thanks for the book Symbolic Logic (Xu, 2008) very much, and all the basic concepts come from it.