LEO-II v2.3.1 -- what is new (October 2026)

Proof output.  A derivation's leaves now name formulas of the problem, as
TSTP requires.  The search is that of v2.3.

* A proof that uses instances of an axiom over sets of properties was not a
  valid derivation in v2.3: each instance was printed as an axiom whose file()
  source named the original axiom, as if the problem stated the instance.
  v2.3.1 prints the axiom as the problem states it, under its name there, and
  each instance as inferred from it:

    thf(ax1gen,axiom,(![X:...]: ...),file('L.p',ax1gen)).
    thf(1,plain,(...),inference(instantiate_sets,[status(thm)],[ax1gen])).

* A definition's leaf cited the defined symbol, file('L.p',ess), where the
  problem calls the definition ess_def.  This was so in every earlier version;
  the leaf now cites the problem's name.

Checked on 118 proofs, 58 of the ontological-argument dataset (20 of them
using instances) and 60 of the TPTP library: every parent exists, every leaf
names a formula of the problem or its includes, and Leo-III's --syntaxcheck
accepts each derivation.