# `Tptp.Lint.Rules.Conjecture`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/lint/rules/conjecture.ex#L1)

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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*