I found a problem with the usage of sledgehammer's proposed solutions:
sometimes, even if it states "Proof found" and it manages to output an
one-line proof without the "timed-out" assertion, the proposed solution
does not work. This problem arrives to me with a certain frequency. Today,
for example, It happened two times in the same proof.
I am available to help solving this problem.
Paulo Emílio de Vilhena.
This archive was generated by a fusion of
Pipermail (Mailman edition) and