123 and 124 completed, in about 12 and 13 hours respectively. I'm running 156 and 160 now.
Mario On Fri, Feb 14, 2020 at 7:27 AM David A. Wheeler <[email protected]> wrote: > On Thu, 13 Feb 2020 19:33:14 -0800 (PST), Norman Megill <[email protected]> > wrote: > > I worked out an estimate (in hours) for jobs 133-160 based on the theory > > that the time to save a compressed proof is proportional to the run time > of > > 'minimize'. ... > > job160.cmd: mideulem 404.4 > > That's less than 17 days, or only about 2 1/2 weeks. > No big deal. I've had other (non-metamath) process executions take longer. > Computer time is *way* cheaper than human time. > > That said, if we could reasonably break up that proof into smaller > components > instead of its current 334 steps, it would probably be easier to > *understand* > > --- David A. Wheeler > > -- > 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/E1j2crr-0001Mg-Tj%40rmmprod07.runbox > . > -- 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/CAFXXJSv8JW2ES_3OocxgKx824uz8jePvz_5bZfA1yHEKpxnd-A%40mail.gmail.com.
