And thanks to Saveliy Skresanov for providing the script preparejobs.sh that made the process of creating the jobs much easier, and to David A. Wheeler for writing the jobs script to automate the process of launching the jobs.
Norm On Thursday, March 5, 2020 at 9:07:14 PM UTC-5, Norman Megill wrote: > > 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/b568b937-896a-4a73-9a3f-a7d9c5ad7230%40googlegroups.com.
