Re: [isabelle] Sledgehammer - Cannot connect to server

Welcome to the group!

I suspect that you havenât done anything wrong. Rather, the SystemOnTPTP service at Miami appears to be down. You can still use sledgehammer with provers installed on your machine, as long as it is powerful enough. Unfortunately, Vampire is not available for download at the moment either; possibly it will be after CADE in August.

Larry Paulson

> On 24 Jun 2015, at 19:51, Artur Gomes <gomesa at> wrote:
> Hi there,
> I'm starting using Isabelle and I tried to find the answer looking back at
> the mailing list history but I couldn't find anything related to it.
> Well, I'm trying to run the "sledgehammer" but I get the following message:
> Sledgehammering...
> Cannot connect to server.
> "remote_vampire": Error: SystemOnTPTP is not available.
> Could someone give me some tips of what should I do in order to configure
> my computer to use the online service? Just to make clear, it is working
> for local solutions anyway.
> By the way, I'm running Isabelle 2015 on OS X 10.10 (Yosemite).
> Thank you very much indeed.
> Best wishes,
> Artur

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