This bug first appeared in version 0.179. I am still working on it; all I know so far is that somewhere it is incorrectly marking ax-dc as already used by the acdc proof.
Anyway, we will have to discard the jobs already started. If any of them finished, it would still be useful to post how long they ran, to give us an idea of the run times we can expect for the others. Alexander told me job101 took about 20 hr. BTW the first theorem in each job file always ~3atlem4, which I will use to calibrate run times for CPU differences; in his case 3atlem4 took 31 sec. I apologize for the work wasted and am very grateful to David Starner for finding this before we got too deep into the job runs. Norm On Wednesday, February 12, 2020 at 8:18:44 AM UTC-5, Norman Megill wrote: > > On Wednesday, February 12, 2020 at 5:53:59 AM UTC-5, Alexander van der > Vekens wrote: >> >> On Wednesday, February 12, 2020 at 10:00:42 AM UTC+1, David Starner wrote: >>> >>> There might be an error in the minimize command; it found that axdc >>> has a much shorter proof using ax-dc, which is obviously true yet >>> defeats the purpose of the axdc theorem ( >>> http://us.metamath.org/mpegif/axdc.html ) and uses new axioms for that >>> theorem. >>> >>> I think ~axdc must be tagged with "(Proof modification is >> discouraged.)", so that minimize will not touch its proof. This is not an >> error of the minimize command. >> > > David is right, there is something very wrong here. While ~axdc should be > tagged with "(Proof modification is discouraged.)" but isn't, in any case > 'minimize' should not be bringing in the new axiom ~ax-dc. > > We should hold off on any more runs until I determine what is happening > and fix the program. Based on what I find, the jobs may have to be > restarted. > > Thanks, David, this was a good observation. > > 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/0b405e55-4212-4d6c-b0ec-ba7ea1ffd5b6%40googlegroups.com.
