Re: [isabelle] Worrying response from remote_vampire for property of complete_lattice (in Main)

Iâm getting this all the time (though with the development version). My guess is that the version of Vampire in Miami has been updated.

In the development version, cvc4 also goes wrong.


> On 14 Aug 2017, at 15:31, Ian Hayes <Ian.Hayes at> wrote:
> "remote_vampire": The prover derived "False", which could be due to inconsistent axioms (including "sorry"s) or to a bug in Sledgehammer
> ---
> What I'm concerned about is the response from remote_vampire:
> are there inconsistencies in the axioms for a complete lattice,

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