Thanks. Looking at the end of the log file, it seems the job didn't complete. 99.7 hrs seems like an unusual number - could there have been a 100 hr timeout?
Scanning forward through statements... Proof of "mideulem" decreased from 7532 to 7527 bytes using "ad2antrr". 359212.21user 5.68system 99:48:42elapsed 99%CPU (0avgtext+0avgdata 1864856maxresident)k 0inputs+40outputs (0major+667317minor)pagefaults 0swaps BTW each printf in metamath.exe has an fflush(stdout) after it, so presumably there is no buffering that would truncate the log. Anyway, DAW recently started running job160 in parallel as a backup. Since your forward 'minimize' scan didn't complete, your run tells us it will take more than 200 hrs. In any case, for the purpose of set.mm, Thierry has broken up ~mideulem into 3 theorems, and we can minimize those separately. Therefore at this point the only purpose of completing job 160 is to get an actual time to compare to the 403-hr estimate to help future estimates. You don't need to restart your run. We'll let DAW run his for weeks, if he is willing, and see what comes through. Norm On Friday, February 21, 2020 at 12:46:57 AM UTC-5, Mario Carneiro wrote: > > Job 160 is done, after 99.7 hours of CPU time. (I think it was done > yesterday, but I got confused with the state of the process and didn't want > to mess with it.) > > It found one lemma, saving 5 bytes. > > Mario > -- 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/4babd0ca-0ae2-4bc1-bc58-c237fc35b76b%40googlegroups.com.
