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.

Reply via email to