[isabelle] sledgehammer+vampire 4.0 often fails



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
    (* ... *)


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