A file stating no conjecture, or more than one.
A TPTP problem states a set of axioms and a single conjecture. Both departures
are well-formed input and neither is a defect, which is why this is the library's
only :info rule. Both nonetheless determine what a consumer may do with the
file, and any consumer dispatching problems to provers must establish the count
for itself.
No conjecture
A file without a conjecture states no proof obligation: it is a satisfiability
problem, an axiom set, or a problem whose conjecture has been removed. A prover
given one reports Satisfiable rather than Theorem, which a pipeline expecting
a proof obligation may misinterpret as failure.
This half of the rule requires the whole problem, so it applies under
Tptp.Lint.run_unit/2 and declines under Tptp.Lint.run/2. A file that includes
its conjecture rather than stating it does not lack one, and a rule unable to
resolve include would report that it did. This is the purpose of the whole
flag on Tptp.Lint.Context.
It still applies to an axiom set analysed as a unit, where the finding is
self-evident. That reading is correct — the file states no obligation — and the
diagnostic is :info and suppressible by code so that a caller which knows what
it holds can discard it.
Multiple conjectures
Two conjecture statements leave the problem ambiguous: a prover will select one,
and the selection is not determined by the file.
negated_conjecture is counted separately and never triggers this rule, since a
single conjecture negated into clause normal form yields many
negated_conjecture clauses. Counting those would report most of the CNF portion
of the TPTP library.