Re: [isabelle] Sledgehammer: Cannot connect to server.



We use "System on TPTPâ, a service provided by Geoff Sutcliffe of the University of Miami. Apparently we are, by far, the biggest users of this service. The link http://pages.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP appears to be down now.

Conceivably, we shall have to provide such a service ourselves one day. The vampire prover is not available to download at the moment.

Larry Paulson


> On 19 Jun 2015, at 13:48, bnord <bnord01 at gmail.com> wrote:
> 
> Hi,
> 
> some students of mine are complaining about the remote sledgehammer tools not working any more. I also could reproduce this problem. Are they gone for good, are they coming back, have they moved or is there something funky going on?
> 
> Sledgehammer output (Isabelle2014/2015):
> Sledgehammering...
> Cannot connect to remote server.
> "remote_vampire": Error: SystemOnTPTP is not available.
> 
> Cannot connect to remote server.
> "remote_e_sine": Error: SystemOnTPTP is not available.
> 
> Best wishes
>  Benedikt
> 





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