Re: [isabelle] prover remote_vampire not responding
On 14/02/18 17:55, Dr A. Koutsoukou-Argyraki wrote:
> 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 www.tptp.org for
> % When you donate this message will disappear.
> % If you do not donate a random delay might be added to your processing
> % SZS end RequiredInformation
> ERROR: Line 1203 Char 47 Token "~" continuing with "nil_typerep = cons_"
Note that there are two messages: the last line looks line a genuine
error. Maybe due to a change of the remote vampire version; or maybe
that is normal: Jasmin Blanchette should be able to say when he is back
This archive was generated by a fusion of
Pipermail (Mailman edition) and