I worked out an estimate (in hours) for jobs 133-160 based on the theory
that the time to save a compressed proof is proportional to the run time of
'minimize'. Here's how it compares so far, assuming a CPU taking about 30
sec for the 3atlem4 minimization. I'll keep this updated as the logs come
in. Looking at the last few, let's hope my theory is wrong...
est. actual hours
job133.cmd: fourierdlem54 0.8
job134.cmd: icccncfext 1.6
job135.cmd: fourierdlem91 2.6
job136.cmd: fourierdlem49 3.0 3.5
job137.cmd: fourierdlem50 3.3
job138.cmd: fourierdlem93 3.4 4.3
job139.cmd: midexlem 3.6 2.8
job140.cmd: miriso 3.9 1.8
job141.cmd: fourierdlem89 4.2 6.5
job142.cmd: tgbtwnconn1lem3 4.7 2.9
job143.cmd: fourierdlem42 6.3 6.4
job144.cmd: fourierdlem48 10.1
job145.cmd: fourierdlem112 14.1
job146.cmd: fourierdlem64 20.3
job147.cmd: fourierdlem65 24.6
job148.cmd: fouriersw 29.5
job149.cmd: fourierdlem73 31.2
job150.cmd: fourierdlem76 35.0
job151.cmd: ioodvbdlimc1lem1 40.4
job152.cmd: ioodvbdlimc1lem2 35.5
job153.cmd: ioodvbdlimc2lem 38.6
job154.cmd: fourierdlem45 40.3
job155.cmd: fourierdlem111 46.4
job156.cmd: fourierdlem81 47.9
job157.cmd: fourierdlem104 61.3
job158.cmd: fourierdlem103 91.0
job159.cmd: footex 268.8
job160.cmd: mideulem 404.4
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/62b2c34b-8c45-426f-9077-7e27f6f8f236%40googlegroups.com.
