[isabelle] Sledgehammer: "The ATP problem is unprovable"
I'm trying out sledgehammer on some very simple lemmas. For instance:
lemma "(1::nat) > (0::nat)"
All both SPASS and remote_vampire return a proof. However, 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 archive was generated by a fusion of
Pipermail (Mailman edition) and