[isabelle] Sledgehammer: One-line proof reconstruction failed



Dear Jasmin,

I'll happily comply to your appeal :-)

I have attached a theory* which makes the Sledgehammer panel print

  "cvc4": One-line proof reconstruction failed: by smt.
  "spass": One-line proof reconstruction failed: by metis.

... and more of the same. However, the goal can be solved by both
'metis' and 'smt'.

Isabelle2014 correctly suggested 'metis'.

If I call 'sledgehammer [strict]' explicitly, the output for
'remote_vampire' changes to

  "remote_vampire": Try this: by meson (6 ms).

... but 'meson' doesn't appear to solve it.

Cheers
Lars



* nevermind the error at the end of the proof, it is unrelated

Attachment: Scratch.thy
Description: application/extension-thy



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