If ~ footex and ~ mideulem are too long, I may split them into smaller lemmas, and then run minimize on the smaller lemmas.
Alternatively, since geometry is a rather closed domain, we know only the theorems from predicate logic and elementary geometry (and basic set theory) are needed to be considered. Is there a way to do that? > Le 14 févr. 2020 à 04:33, Norman Megill <n...@alum.mit.edu> a écrit : > > > 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'. > > est. actual hours > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/23B4CBE7-A34A-4ACF-A3F3-7DFC75DE3BD3%40gmx.net.