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
On Thu, Feb 20, 2020 at 7:28 PM Norman Megill <[email protected]> wrote:
> All jobs from 101 to 158 have completed. Many thanks to all who
> contributed CPU time! Jobs 159 and 160 are still running, but we will
> handle those manually later. Therefore we are ready to start the final
> analysis.
>
> I put all of the logs except 159 and 160 here:
> http://us2.metamath.org/downloads/min2020-logs.zip
>
> Other links for reference:
> 'minimize' scripts: http://us2.metamath.org/downloads/min2020-jobs.zip
> Job status:
> https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/odjUQM6nBAAJ
> Estimates vs. actual run times:
> https://groups.google.com/d/msg/metamath/1wWqUQ5pJp8/WmovUJiKBAAJ
> 2018 'minimize' scripts:
> http://us2.metamath.org/downloads/min2018-jobs.zip
> 2018 logs: http://us2.metamath.org/downloads/min2018-logs.zip
> <http://us2.metamath.org/downloads/min2018-jobs.zip>
> Before performing the final minimize run, we need to make sure it will do
> what we expect. Below are some greps I used to flag some unusually large
> size reductions that we probably want to look at. (The 'uniq' is to get
> rid of identical lines from the forward and backward 'minimize' scans. I
> also edited out some duplicates where the 'from' number was different for
> the two scans, as well as a couple that I will take care of myself.) If
> anyone identifies other suspicious minimizations (with better grep ranges,
> manual inspection of the logs, etc.), please post here.
>
> Many of the suspect cases are in various mathboxes, and it would be best
> if mathbox users review the minimizations done on their mathboxes.
>
> We should edit set.mm to prevent unwanted minimizations rather than
> editing the final minimize job, so that we don't have to do this same
> analysis for next year's run. For example, ~ eqeq1dALT should have "(Proof
> modification is discouraged.)" in its description to prevent overwriting
> its proof with ~ eqeq1d.
>
> I'm not sure what the best way to maintain the results of the analysis.
> Google Documents is a possibility, but I've never used it; someone else
> would have to volunteer to set it up and post instructions for people like
> me. Alternately, I could maintain a fixed post that I edit as people
> respond to this post, like I did for the job status - maybe I'll start off
> doing that.
>
> In the end I'd like to have each minimization accompanied by a
> recommendation e.g.
>
> job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using
> "mptfzshft".
> Resolution: ok (NM)
>
> job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using
> "eqeq1d".
> Resolution: discourage proof modification of eqeq1dALT (WL)
>
> The initials would indicate who analyzed the case and, if not ok, who will
> make the modification to set.mm.
>
> Norm
>
>
>
> $ grep '[0-9]... to [1-3].. bytes' job*.log | uniq
> job128.log:Proof of "fprodshft" decreased from 1054 to 209 bytes using
> "mptfzshft".
>
> $ grep '[2-9].. to [4-9]. bytes' job*.log | uniq
> job102.log:Proof of "ncolne2" decreased from 304 to 53 bytes using
> "ncolcom".
> job104.log:Proof of "gsumsn2" decreased from 351 to 45 bytes using
> "gsumsnd".
> job109.log:Proof of "fz0hash" decreased from 207 to 98 bytes using
> "hashfz0".
> job115.log:Proof of "signswbase" decreased from 257 to 86 bytes using
> "grpbase".
> job132.log:Proof of "euhash1" decreased from 514 to 93 bytes using
> "hashen1".
> job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using
> "ioodvbdlimc1lem
>
> $ grep 'to [1-3]. bytes' job*.log | uniq
> job101.log:Proof of "bj-bi3ant" decreased from 84 to 21 bytes using
> "bi3antOLD".
> job101.log:Proof of "eqeq1dALT" decreased from 144 to 17 bytes using
> "eqeq1d".
> job102.log:Proof of "bj-abf" decreased from 45 to 12 bytes using "abf".
> job102.log:Proof of "frege53aid" decreased from 58 to 33 bytes using
> "com12".
> job102.log:Proof of "ifeq123d" decreased from 174 to 25 bytes using
> "ifbieq12d".
> job102.log:Proof of "mplrcl" decreased from 170 to 38 bytes using
> "strov2rcl".
> job103.log:Proof of "frege24" decreased from 55 to 19 bytes using
> "rp-frege24".
> job103.log:Proof of "hashssle" decreased from 447 to 19 bytes using
> "hashss".
> job103.log:Proof of "tsor2" decreased from 55 to 39 bytes using "imori".
> job104.log:Proof of "aevALT" decreased from 90 to 14 bytes using "aev".
> job104.log:Proof of "frege25" decreased from 55 to 20 bytes using
> "rp-frege25".
> job104.log:Proof of "tsor3" decreased from 59 to 39 bytes using "imori".
> job106.log:Proof of "gsumsndf" decreased from 351 to 29 bytes using
> "gsumsnfd".
> job107.log:Proof of "perpdrag" decreased from 420 to 36 bytes using
> "perpdragALT".
> job108.log:Proof of "leimnltd" decreased from 50 to 19 bytes using
> "lensymd".
> job108.log:Proof of "orcomdd" decreased from 60 to 31 bytes using "syl6".
> job109.log:Proof of "bj-bisym" decreased from 39 to 18 bytes using
> "bisymOLD".
> job109.log:Proof of "fseq0hash" decreased from 88 to 16 bytes using
> "ffzohash".
> job109.log:Proof of "symgfixfvh" decreased from 116 to 32 bytes using
> "fvtresfn".
> job110.log:Proof of "bj-hbsb3" decreased from 50 to 15 bytes using "hbsb3".
> job110.log:Proof of "bj-nfs1" decreased from 42 to 14 bytes using "nfs1".
> job110.log:Proof of "frege55aid" decreased from 30 to 14 bytes using
> "bicom1".
> job110.log:Proof of "sbequ8ALT" decreased from 72 to 15 bytes using
> "sbequ8".
> job111.log:Proof of "frege55b" decreased from 138 to 15 bytes using
> "equcomi".
> job112.log:Proof of "equsb3ALT" decreased from 96 to 15 bytes using
> "equsb3".
> job112.log:Proof of "rp-simp2" decreased from 33 to 14 bytes using "simp2".
> job113.log:Proof of "rp-simp2-frege" decreased from 39 to 34 bytes using
> "rp-a1i".
> job114.log:Proof of "cleqf" decreased from 59 to 35 bytes using "nfcrii".
> job114.log:Proof of "vdgfrgra0" decreased from 495 to 17 bytes using
> "vdfrgra0".
> job115.log:Proof of "AnelBC" decreased from 61 to 32 bytes using "nelir".
> job115.log:Proof of "nfnfcALT" decreased from 89 to 15 bytes using "nfnfc".
> job116.log:Proof of "rexbidvaALT" decreased from 26 to 20 bytes using
> "rexbidva".
> job116.log:Proof of "sbceq1ddi2" decreased from 105 to 38 bytes using
> "sbceq1ddi".
> job116.log:Proof of "wl-equsal" decreased from 86 to 18 bytes using
> "equsal".
> job117.log:Proof of "adant423" decreased from 56 to 39 bytes using
> "sylancom".
> job117.log:Proof of "frege39" decreased from 56 to 34 bytes using
> "rp-frege2i".
> job117.log:Proof of "rexbidvALT" decreased from 25 to 19 bytes using
> "rexbidv".
> job118.log:Proof of "pirp2" decreased from 72 to 30 bytes using "elrpii".
> job119.log:Proof of "rp-frege2ii" decreased from 47 to 37 bytes using
> "rp-frege2i".
> job120.log:Proof of "eleq2dALT" decreased from 165 to 17 bytes using
> "eleq2d".
> job120.log:Proof of "frege57aid" decreased from 58 to 11 bytes using "bi2".
> job120.log:Proof of "impel" decreased from 61 to 35 bytes using "syl2anr".
> job120.log:Proof of "rp-frege2iii" decreased from 51 to 32 bytes using
> "rp-frege2ii".
> job122.log:Proof of "cbvald" decreased from 41 to 34 bytes using "nfvd".
> job123.log:Proof of "ex3" decreased from 53 to 35 bytes using "3impa".
> job124.log:Proof of "3expc" decreased from 26 to 16 bytes using "exp31".
> job124.log:Proof of "dral1ALT" decreased from 81 to 16 bytes using "dral1".
> job124.log:Proof of "frege58bcor" decreased from 64 to 16 bytes using
> "spsbim".
> job125.log:Proof of "dveeq2ALT" decreased from 41 to 15 bytes using
> "dveeq2".
> job125.log:Proof of "tgiooss" decreased from 218 to 17 bytes using
> "rerest".
> job125.log:Proof of "wl-sb6nae" decreased from 63 to 13 bytes using "sb4b".
> job126.log:Proof of "adantlllr" decreased from 47 to 21 bytes using
> "adantl3r".
> job126.log:Proof of "ax12a2" decreased from 55 to 26 bytes using "ax12v".
> job127.log:Proof of "absnpncand" decreased from 148 to 21 bytes using
> "abs3difd".
> job127.log:Proof of "ad5ant1345" decreased from 54 to 21 bytes using
> "adantl3r".
> job127.log:Proof of "ax16nfALT" decreased from 45 to 16 bytes using
> "ax16nf".
> job130.log:Proof of "bf-frege55a" decreased from 73 to 23 bytes using
> "bj-frege55lem2a".
> job130.log:Proof of "bj-csbprc" decreased from 157 to 15 bytes using
> "csbprc".
> job130.log:Proof of "nn0ge2m1nnALT" decreased from 172 to 17 bytes using
> "nn0ge2m1nn".
> job131.log:Proof of "bf-frege55cor1a" decreased from 74 to 14 bytes using
> "bicom1".
> job131.log:Proof of "ccat2s1fvwALT" decreased from 477 to 21 bytes using
> "ccat2s1fvw".
> job131.log:Proof of "wl-sbal1" decreased from 97 to 15 bytes using "sbal1".
> job132.log:Proof of "4an31" decreased from 67 to 37 bytes using "sylanb".
> job132.log:Proof of "frege52b" decreased from 42 to 16 bytes using
> "sbequi".
> job132.log:Proof of "wl-sbal2" decreased from 97 to 15 bytes using "sbal2".
>
> --
> 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/67c66042-7193-4eec-abd2-db9e3d0364ca%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/67c66042-7193-4eec-abd2-db9e3d0364ca%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAFXXJSvNCy0YzYB8663RwHkebfUAAYfexzHZX%3DQXDvtAJXXcGA%40mail.gmail.com.
Metamath - Version 0.181 12-Feb-2020 Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 37327684 bytes
37327684 bytes were read into the source buffer.
The source has 174136 statements; 2483 are $a and 34733 are $p.
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
if you want to check them.
MM> submit 'metamathjobs/job160.cmd'
Taking command lines from file "metamathjobs/job160.cmd"...
MM> ! 3atlem4 is used as reference for CPU speed calibration
MM> prove 3atlem4
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT 3atlem4"):
155429 3at.l $e |- .<_ = ( le ` K ) $.
155430 3at.j $e |- .\/ = ( join ` K ) $.
155431 3at.a $e |- A = ( Atoms ` K ) $.
155435 3atlem4 $p |- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e.
A /\ T e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) /\ ( ( P .\/ Q )
.\/ R ) .<_ ( ( S .\/ T ) .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/
T ) .\/ R ) ) $= ... $.
Note: The proof you are starting with is already complete.
MM-PA> minimize_with * /allow_new_axioms * /no_new_axioms_from ax-* /time
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
No shorter proof was found.
(Other mathboxes were not checked. Use / INCLUDE_MATHBOXES to include them.)
MINIMIZE_WITH run time = 35.11 sec for "3atlem4"
MM-PA> _exit_pa /force
Exiting the Proof Assistant. Type EXIT again to exit Metamath.
MM> ! start of main run
MM> prove mideulem
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT mideulem"):
$d x .- $. $d x A $. $d x B $. $d x I $. $d x O $. $d x P $. $d x Q $.
$d x T $. $d ph x $.
97509 colperpex.p $e |- P = ( Base ` G ) $.
97510 colperpex.d $e |- .- = ( dist ` G ) $.
97511 colperpex.i $e |- I = ( Itv ` G ) $.
97512 colperpex.l $e |- L = ( LineG ` G ) $.
97513 colperpex.g $e |- ( ph -> G e. TarskiG ) $.
97582 mideu.s $e |- S = ( pInvG ` G ) $.
97583 mideu.1 $e |- ( ph -> A e. P ) $.
97584 mideu.2 $e |- ( ph -> B e. P ) $.
97598 mideulem.1 $e |- ( ph -> A =/= B ) $.
97599 mideulem.2 $e |- ( ph -> Q e. P ) $.
97600 mideulem.3 $e |- ( ph -> O e. P ) $.
97601 mideulem.4 $e |- ( ph -> T e. P ) $.
97602 mideulem.5 $e |- ( ph -> ( A L B ) ( perpG ` G ) ( Q L B ) ) $.
97603 mideulem.6 $e |- ( ph -> ( A L B ) ( perpG ` G ) ( A L O ) ) $.
97604 mideulem.7 $e |- ( ph -> T e. ( A L B ) ) $.
97605 mideulem.8 $e |- ( ph -> T e. ( Q I O ) ) $.
97606 mideulem.9 $e |- ( ph -> ( A .- O ) ( leG ` G ) ( B .- Q ) ) $.
97607 mideulem $p |- ( ph -> E. x e. P B = ( ( S ` x ) ` A ) ) $= ... $.
Note: The proof you are starting with is already complete.
MM-PA> minimize_with * /allow_new_axioms * /no_new_axioms_from ax-* /time
Bytes refer to compressed proof size, steps to uncompressed length.
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
