SInE Premise Selection

SInE (Sumo Inference Engine) is a premise selection algorithm that filters large axiom sets down to a relevant subset before the search begins. It was introduced by Hoder and Voronkov (2011) and is used by most modern ATP systems (E, Vampire) for large-theory problems.

Prover9's SInE implementation selects axioms based on symbol sharing with the goal formulas, using a breadth-first search (BFS) with configurable tolerance and depth. Axioms that share rare symbols with the goals are selected first, and the process propagates outward.

SInE is designed for TPTP problems with many axioms. It is completely inert in LADR mode — all defaults are no-ops when reading native LADR input.

Auto-Enable Conditions

SInE auto-enables (with the default assign(sine, -1)) when all of the following are true:

TPTP input mode is active.
The input contains more than 128 axioms.
The input contains at least one goal (conjecture) formula.

If any condition is not met, SInE is silently skipped. To force SInE on or off regardless of auto-detection, use an explicit assign(sine, N) value (see Options).

Operating Modes

SInE operates in one of two modes depending on the number of axioms in the input.

Soft Filter Mode (≤5000 axioms)

When the axiom count is 5000 or fewer, SInE uses a safe soft filter:

All SInE-selected axioms go to SOS (the active search set).
All unselected axioms go to usable (available for inference but not selected as given clauses).
No axioms are discarded.

This is safe because unselected axioms remain available in usable for back demodulation, unit deletion, and other simplification operations. In this mode, sine_weight is auto-set to 100 (if not explicitly assigned), causing the given-clause selector to prefer axioms closest to the goal.

Depth-Based Mode (>5000 axioms)

When the axiom count exceeds 5000, SInE uses a more aggressive depth-based filter:

BFS depth 1–2 axioms passing the tight threshold (150 / 1.5×) go to SOS.
BFS depth 3 axioms passing only the wide threshold (200 / 2.0×) go to usable.
Axioms below both thresholds are discarded entirely.

Parameters are auto-adjusted: BFS depth is limited to 3, and two tolerance thresholds are used. The original tolerance (200 / 2.0×) is kept as a wide threshold. Axioms passing the tight threshold (150 / 1.5×) are "tightly selected" and go to SOS. Axioms passing only the wide threshold are "loosely selected" and go to usable. Axioms below both thresholds are discarded.

Options

`assign(sine, N)`

SInE tolerance control. Default: -1 (auto-enable).

Value	Behavior
`-1`	Auto-enable for TPTP input with >128 axioms and a conjecture. Sets tolerance to 200 (2.0×).
`0`	Disable SInE entirely.
`>0`	Enable with explicit tolerance as a percentage: 200 = 2.0×, 150 = 1.5×, 100 = 1.0× (exact match only).

An axiom is selected if it contains a symbol s where:

occurrence_count(s) ≤ tolerance × min_occurrence_in_axiom

Lower tolerance values select fewer axioms.

`assign(sine_depth, N)`

BFS depth limit for SInE propagation. Default: 0 (run to fixpoint).

Value	Behavior
`0`	Run BFS until no new axioms are selected (fixpoint).
`>0`	Limit BFS to N levels. Depth 1 = axioms sharing symbols with goals. Depth 2 = axioms sharing symbols with depth-1, and so on.

`assign(sine_weight, N)`

Depth-based clause weight penalty. Default: 0 (disabled).

When set to a positive value, adds N × (depth - 1) to the weight of each clause derived from a SInE-selected axiom. Depth-1 axioms (closest to the goal) get no penalty; depth-2 get +N; depth-3 get +2N. This causes the given-clause selector to prefer tightly related clauses.

Auto-set to 100 in both soft filter and depth-based modes.

`assign(sine_max_axioms, N)`

Maximum number of axioms to select. Default: 0 (unlimited).

When set to a positive value, BFS stops early once the selected axiom count reaches N. Primarily used by the strategy scheduler to give different children different selection sizes.

Command-Line Flags

Flag	Effect
`-nosine` / `-no-sine` / `-no_sine`	Disable SInE. Equivalent to `assign(sine, 0)`. Also disables multi-ordering trial.

You can also disable SInE from a TPTP file using a magic comment:

% prover9: assign(sine, 0).

Symbol Exclusions

To avoid spurious cross-linking of unrelated axioms, two categories of symbols are excluded from SInE's occurrence counting:

Equality (=). Equality appears in virtually every equational axiom, so counting it would link all equational axioms regardless of subject matter.
Variables. In TPTP's Prolog-style convention, variables are uppercase symbols that appear in every formula. Counting them would link everything.

This follows the standard practice of E prover and Vampire.

Hypothesis Role Seeding

TPTP formulas with role hypothesis are treated specially: they are pre-selected (seeded) at BFS depth 1, the same as goals. This means hypothesis formulas are always included and their symbols seed the BFS propagation, helping to select axioms relevant to both the conjecture and any problem-specific hypotheses.

Interaction with Other Features

Strategy scheduling: The sliding-window scheduler (-cores N) gives each child different SInE parameters (tolerance, depth, max_axioms) for diversity.
Checkpoint/resume: SInE runs during preprocessing, before the search begins. A checkpoint captures the post-SInE clause set. On resume, SInE does not re-run.
Multi-ordering trial: Runs after SInE, before the search. SInE filtering reduces the symbol count, which can change the optimal precedence ordering.
LADR mode: All SInE options are inert. No axioms are filtered, no weights are adjusted, no auto-enable occurs.

Diagnostic Output

SInE prints diagnostic information to stderr when it runs.

Soft-filter mode:

% SInE: 342 to sos, 786 to usable, of 1128 axioms
  (tolerance 200, depth 0 [fixpoint]).

Depth-based mode:

% SInE (scan): 156 to sos (tol 1.5x), 412 to usable (tol 2.0x), 37673 zapped, of 38241 axioms (depth 3).

The "sos" count is tightly selected axioms. The "usable" count is loosely selected axioms. "Zapped" axioms are discarded.

Examples

Example 1: Default (auto-enable for large TPTP inputs)

prover9 -t 60 -f large_problem.p

If large_problem.p has more than 128 axioms and a conjecture, SInE activates automatically with tolerance 200 (2.0×).

Example 2: Explicit tolerance via magic comment

% prover9: assign(sine, 150).

fof(ax1, axiom, ...).
...
fof(goal, conjecture, ...).

Tolerance 150 (1.5×) selects fewer axioms than the default 200.

Example 3: Disable SInE

prover9 -nosine -t 60 -f large_problem.p

Disables SInE even for large inputs. Equivalent to the magic comment % prover9: assign(sine, 0).

Example 4: Tune depth and weight

% prover9: assign(sine, 200).
% prover9: assign(sine_depth, 5).
% prover9: assign(sine_weight, 50).

Tolerance 2.0×, BFS depth 5, weight penalty of 50 per depth level.

Performance

SInE provides the most benefit on problems with thousands of axioms where most axioms are irrelevant to the conjecture:

Axiom Count	Typical Speedup
~1,000	2–10×
~10,000	10–50×
~38,000	Enables proofs that would otherwise time out

For problems with fewer than ~100 axioms, SInE overhead is minimal but the benefit is negligible.

References

Hoder, K. and Voronkov, A. "Sine Qua Non for Large Theory Reasoning." Proceedings of CADE-23, LNAI 6803, pp. 299–314, 2011.

Sutcliffe, G. "The TPTP Problem Library." http://www.tptp.org

Next Section: Strategy Scheduling