Re: [isabelle] Sledgehammer: "The ATP problem is unprovable"
Am 13.04.2012 um 03:02 schrieb John Munroe:
> I'm trying out sledgehammer on some very simple lemmas. [...] For
> lemma "(1::real) > (0::real)"
> E works fine, but both SPASS and remote_vampire fail. For SPASS, I get
> "The ATP problem is unprovable" while remote_vampire gives "An ATP
> error occurred". Is there something wrong with my set up or are SPASS
> and remote_vampire really this weak?
This is strange. Perhaps it depends on the theories imported. I just tried
lemma "(1::real) > (0::real)"
sledgehammer [remote_vampire spass e]
with Isabelle2011-1 (and a recent repository version), and all three provers were quick to find the proof
by (metis zero_less_one)
very quickly. If you want to investigate this further, please send me a complete ".thy" file and Sledgehammer's output with the "debug" option:
This archive was generated by a fusion of
Pipermail (Mailman edition) and