Stream: Beginner Questions

Topic: Sledgehammer finds proof metis times out

view this post on Zulip Hanna Lachnitt (Jul 02 2022 at 21:31):

Hi,
does someone has an example for me where sledgehammer proposes a proof but metis times out on it? I feel I encounter them all the time just not when I actually want one :grinning_face_with_smiling_eyes:

view this post on Zulip Albert Jiang (Jul 03 2022 at 16:14):

Hanna Lachnitt said:

Hi,
does someone has an example for me where sledgehammer proposes a proof but metis times out on it? I feel I encounter them all the time just not when I actually want one :grinning_face_with_smiling_eyes:

Maybe try increasing the metis timeout limit a bit to see if that resolves the problem?

Last updated: Feb 01 2025 at 20:19 UTC