All minimization runs are now incorporated into set.mm. The total size reduction of set.mm was 217484 bytes. set.mm now contains 2684 fewer lines.
Notes: (1) The byte count above is for set.mm on Linux. On Windows, the reduction was 220168 bytes because of the extra byte in the CR/LF line termination. (2) Thierry broke up the large proof in job160 into smaller lemmas and minimized them separately, so I didn't include job160 in the total. Many thanks to the following people who donated CPU time for these runs: Thierry Arnoux Mario Carneiro heiphohmia Giovanni Mascellani David Starner Alexander van der Vekens David A. Wheeler Also, thanks to the people on this thread who analyzed the results for suspicious minimizations. The numbers above reflect the adjustments that were made as a result of that analysis. Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/acf87361-ccde-4147-b540-7b2cc64d6886%40googlegroups.com.
