I conducted some tests on the new theorems, targeting the commands that would typically cause metamath-exe to get stuck. These are the time reports:

show proof footexlem1 /compressed -> t = 0.14 s
show proof footexlem2 /compressed-> t = 0.22 s
show proof footex /compressed -> t = 0.94 s

show proof footexlem1 /normal -> t = 0.83 s
show proof footexlem2 /normal -> t = 1.41 s
show proof footex /normal -> t = 5.89 s

save proof footexlem1 /compressed -> t = 0.04 s
save proof footexlem2 /compressed -> t = 0.04 s
save proof footex /compressed -> t = 0.67 s

save proof footexlem1 /normal -> t = 0.04 s
save proof footexlem2 /normal -> t = 0.06 s
save proof footex /normal -> t = 0.63 s

prove footexlem1 -> t = 0.12 s
MINIMIZE_WITH * /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM ax-* -> t = 77.47 s
save new_proof /normal -> t = 0.01 s
save new_proof /compressed -> t = 0.01 s

prove footexlem2 -> t = 0.11 s
MINIMIZE_WITH * /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM ax-* -> t = 132.39 s
save new_proof /normal -> t = 0.03 s
save new_proof /compressed -> t = 0.02 s

prove footex -> t = 0.33 s
MINIMIZE_WITH * /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM ax-* -> t = 592.35 s
save new_proof /normal-> t = 0.43 s
save new_proof /compressed -> t = 0.49 s

It's quite evident that the revision in this PR is a substantial improvement over the old state.

Only note: ~ footexALT will be annoying when executing save proof * /compressed which as shown here is worth doing once in a while. I think in the long term ~ footexALT should be deleted.

Too bad I did not see your issues with ~footex earlier @GinoGiotto, if I had done that change earlier it would have spared you quite some computing power and time.

I think ideally we should try to reproduce that case and keep it in a separated test/stress database, but I currently don't see how without pulling a substantial part of set.mm, or better identifying what made that proof so special.

Too bad I did not see your issues with ~footex earlier @GinoGiotto, if I had done that change earlier it would have spared you quite some computing power and time.

My initial intention with the second attempt was to produce a log file and report it as an issue (basically I wanted to see if metamath-exe writes something before crashing), but since it proceeded without interruptions I simply committed the shortened proof instead.

I think ideally we should try to reproduce that case and keep it in a separated test/stress database, but I currently don't see how without pulling a substantial part of set.mm, or better identifying what made that proof so special.

Temporarily it might be enough a simple TODO note, like "Delete and extract a test case once its time-draining nature has been examined".

Only note: ~ footexALT will be annoying when executing save proof * /compressed which as shown here is worth doing once in a while. I think in the long term ~ footexALT should be deleted.

~ footexALT should be kept until the "problem" with metamath.exe is solved. It has a "(Proof modification is discouraged.)" tag, so a global minimization will not touch it, and I do not see a need to perform a global save proof * /compressed (save proof * /compressed/fast seems to be not affected).