improve Vampire's Prolog compliance

[MichaelRawson]

Various downstream tools (mostly my own lol, but not entirely) rely on Vampire's TSTP output being valid Prolog data (modulo some TPTP operator definitions).

It almost is. Fix a few remaining edge cases, discovered with the help of Scryer Prolog's relatively strict ISO implementation:

1. clauses cannot occur as a top-level argument (because of the disjunction operator's precedence), they need parenthesising
2. ~$true tokenises as ~$, true. Write this as ~ $true, which is the intended ~, $, true
3. ~(A & B) reads as function application (!). Also add a space after negation here.

@geoffgeoffgeoff3 may also be interested, but perhaps he has transcended Prolog.

[geoffgeoffgeoff3]

I'm interested, but maybe less than I would have been 20 years ago when TPTP2X was the tool of choice for processing TPTP annotated formulae. Now I rely on TPTP4X more. Things were initially developed to run on under SICStus Prolog, then Eclipse, and now SWI. Seems that Scryer is a bit more anal, but that's prolly not a bad thing. If you can tweek my operator definitions to make things work in both SWI and Scryer, you will be making the world a better place. Anyhoo ...

1. fof(1,axiom,p | q). and cnf(1,axiom,p | q). work fine for me,
2. I confirm that ~$true does not parse, and the space is necessary ~ $true. SWI agrees.
3. fof(1,axiom,~(p & q)). works fine for me.

[MichaelRawson]

I do not have access to the Prolog standard, so some of the below information is LLM-sourced and therefore maybe-hallucinated (what a time to be alive). But it's self-consistent and consistent with the Scryer/Trealla implementations.

1. They do in SWI, but if you try this in e.g. Scryer is will not work. This is because | has precedence 1102, which is higher than the "argument position" precedence, 999. You cannot apparently give a precedence less than 999, something about the list operator [_ | _].
2. Good. :)
3. This one is actually the same issue in disguise, but yet more pedantic. If you put symbols (even operators) directly next to the argument list, it gets "pre parsed" as a function application. Then the arguments need to have priority 999 or less. However, with the extra space it's an operator and therefore OK. SWI and Scryer accept this, but not Trealla.

None of this can actually be fixed in TPTP2X, we just have to be pedantic about printing if we want to be read by Prolog - although we could debate whether the TPTP grammar should be changed to reflect Prolog's constraints.