*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] sledgehammer+vampire 4.0 often fails*From*: Christoph Dittmann <f-isabellelist at yozora.eu>*Date*: Mon, 23 May 2016 16:54:26 +0200

Hi, I have a problem with sledgehammer in Isabelle 2016 with a recent vampire: ./vampire --version Vampire 4.0 (commit 910b0ff on 2016-04-14 14:40:26 +0200) I added the vampire binary to Isabelle by setting these environment variables, as documented in sledgehammer.pdf: export VAMPIRE_HOME=$HOME/local/bin export VAMPIRE_VERSION=4.0 Very often (I guess in >50% of the cases), vampire fails like this: Sledgehammering... "e": Try this: using Cons.prems(2) by auto (20 ms). "spass": Try this: using Cons.prems(2) by auto (4 ms). "vampire": A prover error occurred. (Pass the "verbose" option for details.) When I look at the output of vampire, it says: User error: Vampire only supports a single conjecuture in a problem And it's true, the vampire input file generated by sledgehammer sometimes ends with more than one conjecture, for example: % Conjectures (2) tff(conj_0, conjecture, ($false)). tff(conj_1, conjecture, ((?[N4 : nat]: (pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat, N4), aa_list_a_nat(size_size_list_a, cons_a(x, xsa)))) & (pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat, N4), aa_list_a_nat(size_size_list_a, ysa))) & (~ aa_nat_a(aa_list_a_fun_nat_a(nth_a, cons_a(x, xsa)), N4) = aa_nat_a(aa_list_a_fun_nat_a(nth_a, ysa), N4))))))). I attached a minimal theory file that shows the problem. Is this a known problem? Is there anything I can do? Thanks, Christoph

theory Foo imports Main begin lemma list_prefix_decomp: shows "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys' \<and> (xs' = Nil \<or> ys' = Nil \<or> hd xs' \<noteq> hd ys')" proof- { text {* Exclude some trivial cases. *} assume "\<not>(\<exists>ys'. ys = xs @ ys')" "\<not>(\<exists>xs'. xs = ys @ xs')" "xs \<noteq> ys" text {* Determine an index where the lists diverge. *} hence "\<exists>n. n < length xs \<and> n < length ys \<and> xs ! n \<noteq> ys ! n" proof(induct xs arbitrary: ys, simp) case (Cons x xs ys) show ?case proof(cases) assume "ys = Nil" thus ?thesis sledgehammer (* ... *)

**Follow-Ups**:**Re: [isabelle] sledgehammer+vampire 4.0 often fails***From:*Jasmin Blanchette

- Previous by Date: [isabelle] Problem with "additional type variables" in a definition
- Next by Date: Re: [isabelle] sledgehammer+vampire 4.0 often fails
- Previous by Thread: Re: [isabelle] Problem with "additional type variables" in a definition
- Next by Thread: Re: [isabelle] sledgehammer+vampire 4.0 often fails
- Cl-isabelle-users May 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list