[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] Is remote ATP solving server now down?



I try to use "by;" trigger for remote solving. I use this correct article as a test-case:

environ
begin
1=1;

But when I try (in Emacs with Mizar mode) to type by; instead of ; to auto-complete proof I receive the following message:

ATP-Unsolved; :: [ATP details]

and the details are:

HTTP/1.1 200 OK
Date: Sat, 21 Feb 2015 11:36:00 GMT
Server: Apache/2.2.20 (Ubuntu)
Vary: Accept-Encoding
Keep-Alive: timeout=5, max=100
Connection: Keep-Alive
Transfer-Encoding: chunked
Content-Type: text/html; charset=ISO-8859-1

sh: bin5.29.1227/mizf: not found

==========

==========

==========

==========
Request took 0s

Any ideas?

Regards,
Boris