Re: [isabelle] Sledgehammer on Windows



Hello,

I've started up my Windows 8 VM (in VirtualBox, using 4 GB of RAM,
single core) and installed RC3. Here are my findings, should they be
helpful to anyone:


lemma "[a] = [b] â a = b"

With "try methods" enabled:

"remote_vampire": Error: SystemOnTPTP is not available.
"z3": Try this: by simp (0.0 ms).
"spass": Try this: by auto (0.0 ms).
"e": Try this: by simp (0.0 ms).

With "try methods" disabled:

"cvc4": Try this: by (metis list.inject) (0.0 ms).
"remote_vampire": Try this: by (metis list.inject) (0.0 ms).
"z3": Try this: by (metis list.inject) (15 ms).
"spass": Try this: by (metis list.inject) (0.0 ms).
"e": Try this: by (metis the_elem_set) (156 ms).


lemma "m < n+1 âsetsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"

"cvc4": Try this: by (smt ... a bunch of facts ...) (235 ms).
"remote_vampire": Timed out.
"z3": Try this: by (simp add: add.commute atLeastAtMostPlus1_int_conv)
(109 ms).
"spass": Timed out.
"e": Timed out.


Cheers
Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.