Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle RC4 and Sledgehammer on Windows


view this post on Zulip Email Gateway (Aug 22 2022 at 09:45):

From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius and Jasmin,

Some initial results with sledgehammer on Windows (RC4) using the
standard configuration.

(1) lemma "[a] = [b] ==> a = b"
(2) lemma aux: "m < n+ ==> setsum f {m..n + 1} =
setsum f {m..n} + f (n + 1 ::
int)"

Best!


Lemma (1)

"remote_vampire": Try this: by (metis list.inject) (16 ms).
"z3": Timed out.
"cvc4": Timed out.
"spass": Timed out.
"e": Try this: by (metis list.inject) (63 ms).


Lemma (1) tried a second time

"z3": Try this: by (metis list.inject) (469 ms).
"spass": Timed out.
"cvc4": Timed out.
"remote_vampire": Try this: by (metis list.inject) (16 ms).
"e": Try this: by (metis list.sel(1)) (32 ms).


Lemma (1) using fact_filter=mepo

"spass": Timed out.
"remote_vampire": Try this: by (metis list.inject) (109 ms).
"z3": Try this: by (metis list.inject) (63 ms).
"cvc4": Timed out.
"e": Try this: by (metis the_elem_set) (31 ms).


Lemma (2) tried twice and a third time using fact_filter=mepo

"spass": Timed out.
"z3": Timed out.
"cvc4": Timed out.
"remote_vampire": Timed out.
"e": Timed out.



Last updated: Mar 28 2024 at 08:18 UTC