On Wednesday, February 12, 2020 at 10:05:48 PM UTC-5, David Starner wrote: > > Given about 8 hours a run for me, I'll take two batches of 8; 103-111 and > 135 to 143. >
That would be great. Just be aware that some or many of 133 and above (with 1 theorem each) are expected to take much more than 8 hrs, possibly weeks. We just don't know, although roughly the run times are expected to increase as the job number goes up. Basically you are exploring new territory above 132. For jobs that are taking, say, more than a week (or however long your patience lasts), you may want to abort them, and we can investigate alternate approaches (ranging from running 'minimize' on small statement ranges to breaking up the proof into lemmas - I would prefer breaking up the proof to benefit future runs but that's hard work). If a job is aborted, we can still apply any minimizations it did find. 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/fe247a33-2a8f-4cc2-88bf-a8e3574dd3e3%40googlegroups.com.
