The structured set of higher-order problems from examples/structured_hol_problems.livemd, expressed as self-contained TPTP THF problem strings.

The livebook states its problems in a mixture of ~f (bare formula, types inferred), ~e/with_context (formula plus an ambient type environment) and ~p (TPTP problem). To compare ShotTx against external provers, every problem here is normalised to one representation: a complete THF problem that both ShotDs.Tptp.parse_tptp_string!/1 and SystemOnTPTP accept verbatim. Nobody gets a different input.

Two deliberate deviations from the livebook text:

• Monomorphisation. The livebook declares l: A > A > $o and friends with implicit type variables. Rank-1 polymorphism is TH1, which Satallax and E do not accept, so every equality-like relation is declared at a concrete type. Where the livebook applies one polymorphic constant at two different types (e.g. l @ F @ G and l @ (F @ X) @ (G @ X) in Example 9a), this suite declares two monomorphic copies (l_f, l_i).

• Set-theory typo fix. set_theory_defs in the livebook defines set_l1 three times and never defines set_l2, set_l3, set_set_l2 or set_set_l3 — a copy-paste slip that leaves the Example 22 Leibniz variants referring to undefined constants (hence not theorems at all). Each definition here binds its own head.

Free set constants in Example 22 are named sa/sb/sc throughout so the Andrews variant, which needs the constant a for its own relation, does not collide.

Each problem carries the livebook's own annotation in :note ("THM", "Timeout", or "" where the livebook made no claim). That is the author's recorded observation, not ground truth — the reference provers supply that.