Error in the tptp_to_ladr utility

[letalvoj]

Hi,

while using prover9 / mace4 together with TPTP language I found a bug in the tptp_to_ladr utility. If you put negation into an axiom directly before an existential quantifier than the axiom is not translated correctly.

For example:

fof(a, axiom, ( a <=> (~?[X]:(p(X))) )).
fof(b, axiom, ( b <=> ~(?[X]:(p(X))) )).

a <-> p(X) # label(a) # label(axiom).
b <-> -(exists X p(X)) # label(b) # label(axiom).

This repo seems to be dead but I put it here for other people who might experience the same problem.
V.

[jessealama]

Thanks for the report.