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
> i.e.
>  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
> 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_"

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
from vacation.


	Makarius





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