On Fri, Feb 14, 2020 at 3:12 PM Norman Megill <[email protected]> wrote: > A simple way to fix this is to add "(Proof modification is discouraged.)" to > dral1ALT, etc. as they should have anyway. Then the final 'minimize' run > will skip them. There are also a number of "suspicious" minimizations on > non-ALT/OLD theorems as can be seen with "grep 'to [12]. bytes' job*.log" > e.g.: > > job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf". > job103.log:Proof of "hashssle" decreased from 370 to 19 bytes using "hashss". > > When everything is done, we will need to analyze these and decide what to do.
That seems correct for hashssle; it takes a hypothesis in hashss 𝐴 ∈ 𝑉 and turns it into 𝐴 ∈ Fin. > Unfortunately these jobs will have to be rerun. The theorems in job133.cmd > through job160.cmd were not changed so those runs shou OK. Does that mean that 125-132 are open again? Since 155 hasn't started running backwards yet, I might as well load up the rest of those cores. -- Kie ekzistas vivo, ekzistas espero. -- 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/CAMZ%3Dzj4F-%3DJLkAf1UAO0Fgw2-5R9Fwr6sbPepOL9XB%2BqQhH2yQ%40mail.gmail.com.
