[isabelle] Sledgehammer: "The ATP problem is unprovable"



Hi,

I'm trying out sledgehammer on some very simple lemmas. For instance:

lemma "(1::nat) > (0::nat)"
sledgehammer

All both SPASS and remote_vampire return a proof. However, for

lemma "(1::real) > (0::real)"
sledgehammer

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?

Thanks

John





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