8 Trivial auto-generated theorems

4.2m implications proven by a transitive reduction of 15k theorems were proven using simple rewrite proof scripts.

include more details of the methodology, and any comparisons with other generated implication data sets.