Re: [isabelle] prover remote_vampire not responding

Dear Makarius,

thank you for your answer. By trying the same
 lemma "[x] = [y] ⟹ x = y"
  sledgehammer [prover = remote_vampire, verbose]

I also get an error and moreover I get the following mysterious message:

 "remote_vampire": A prover error occurred:
% SZS start RequiredInformation
% Congratulations - you have become a registered power user of SystemOnTPTP, at IP address 128.232.*. % Please consider donating to the TPTP project - see for details.
% When you donate this message will disappear.
% If you do not donate a random delay might be added to your processing time.
% SZS end RequiredInformation
ERROR: Line 1203 Char 47 Token "~" continuing with "nil_typerep = cons_"


On 2018-02-14 12:48, Makarius wrote:
On 13/02/18 20:06, Dr A. Koutsoukou-Argyraki wrote:

-my threads number was set by default to threads=0. When I changed it to
5, indeed
remote_vampire "appeared" after using sledgehammer but only gave the
"a prover error occurred".

Here is another way to invoke just remote_vampire with more output:

lemma "[x] = [y] ⟹ x = y"
  sledgehammer [prover = remote_vampire, verbose]

This gives me:

"remote_vampire": A prover error occurred:
ERROR: Line 809 Char 31 Token "~" continuing with "Y = nil_typerep) =>"

So it might be again a problem of the vampire "Software-as-a-Service".


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