Email Gateway (Aug 22 2022 at 09:45): 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: Nov 21 2024 at 12:39 UTC