The QFL-Generator takes the formula whose proof is being attempted and produces a growing conjunction of quantifier-free lines in conjunctive normal form. The Processor periodically tests that finite conjunction for consistency. If it is inconsistent, those ground instances constitute a proof of the original formula. If it is consistent, generation resumes with more substitutions.

This is the same layered termination contract as Canon 0072, now expressed as program control. The Processor must finish each finite SAT test. The QFL-Generator may be recalled repeatedly because finite consistency is not a countermodel to the full first-order target. Only an inconsistent prefix terminates the proof attempt successfully.

The split also isolates engineering regimes. Generating terms and tuples is a systematic enumeration problem. Testing the clause database is a mutable data-structure problem. The first controls which evidence arrives; the second controls how aggressively that evidence is compressed. A bottleneck in either half can make a valid theorem unreachable before memory or time is exhausted.

The paper reports a completed IBM 704 program, modifications prompted by programming it and trial results. This matters historically because the algorithm is not treated as a fixed mathematical object whose implementation merely follows. Clause growth, tape latency, table layout and input order feed back into the design. The paper is an early account of algorithm engineering in which representation changes the practical frontier of provability.

Write the current formula as (A∨p)∧(B∨¬p)∧R in the paper's factored notation. Rule III replaces the p-bearing parts by a result equivalent for consistency to (A∨B)∧R. At clause level, every positive p-clause must be paired with every negative p-clause to form a resolvent. If p has m positive and n negative parent clauses, the cross-product can contain mn candidates.

The authors observed two connected pathologies. Repeated applications rapidly increased both the number and total length of clauses, and many generated clauses were duplicates. They programmed systematic redundancy deletion with some success, yet the total-length problem remained on complicated inputs. Fast-access storage, not abstract soundness, made the rule prohibitive.

Rule III also seldom created new one-literal clauses. That deprived the Processor of its cheapest and most decisive reduction. A transformation might eliminate one variable while leaving a broad residue that unit propagation could not immediately collapse. On a machine with 32,768 words of core, width mattered.

This is not evidence that resolution is logically inferior. It is evidence that eager variable elimination has an operational cost profile. The same inference can be useful when bounded elimination or subsumption keeps growth small. The 1962 program needed a rule whose intermediate state matched its storage hierarchy, so it changed how alternatives were represented.

Again write F=(A∨p)∧(B∨¬p)∧R, with A, B and R free of p. If p=false, the first p-clauses reduce to A, the ¬p-clauses are satisfied, and the branch is A∧R. If p=true, the symmetric branch is B∧R. F is inconsistent if and only if both branches are inconsistent.

The proof is a two-case exhaustion of a Boolean atom. Every complete assignment gives p exactly one value, so a satisfying assignment for either branch extends to a model of F. Conversely, a model of F belongs to one branch. This is Rule III* in the primary, later called the splitting rule.

Splitting often creates unit clauses because setting p removes the opposite literal from every threatened clause. Those units enter the ready list and trigger cascades of deletion. The authors contrast this with Rule III, which seldom yielded new units. Branching therefore buys not only smaller immediate state but more opportunities for cheap propagation.

The cost has moved, not vanished. A difficult formula may require both branches at many levels, producing exponential search depth and repeated subproblems. What changed was the materialisation strategy. The program keeps one path active and defers alternatives, allowing fast memory to serve the current branch instead of housing the union of all resolvents.

The tape records are organised in what the paper calls a cafeteria “stack-of-plates”: the last record written is the first read. In contemporary terms, this is a LIFO stack implementing depth-first search. A decision pushes a choice point. A conflict pops the newest untried alternative. Earlier choices remain buried until their descendants have been exhausted.

If processing discovers consistency on the active branch, the program does not immediately explore old alternatives. A consistent finite QFL set means that more ground lines are needed, so the QFL-Generator is recalled. If processing discovers inconsistency, the machine checks the Rule III* tape. With a saved record, it restores the last alternative. With no record, every branch for the current finite clause set has failed and the quantifier-free lines are inconsistent.

This control flow reveals that “consistent” is contextual. It can mean the active finite formula has a model, so outer generation must continue. “Inconsistent” can mean one speculative branch failed, so backtracking is required. Only inconsistency with an empty choice stack proves the entire finite conjunction inconsistent.

Depth-first storage fits the hardware hierarchy because only one working formula occupies core at a time. Tape trades access speed for capacity and recoverability. The stack order is not logically necessary: other complete traversals could work: but it determines which assignments are tried, how quickly a conflict is found and how much state remains resident.

The input matrix is supplied in coded Polish notation: parenthesis-free prefix form. First, truth-functional connectives are rewritten using negation, conjunction and disjunction. Negations move inward by De Morgan laws until they cancel or act directly on atoms. Existentials become function symbols, universals are dropped and the result is placed in conjunctive normal form.

The authors note that conversion to a quantifier-free CNF matrix still required pencil work, though a computer could have performed it. A one-to-one assembler handled the final translation into octal numbers. The distinction is a useful antidote to anachronism: this was a running prover, but not an end-to-end parser and normaliser for arbitrary mathematical prose or unrestricted formulas.

Avoiding prenex form changes the order and dependency structure seen by the generator while preserving the intended proof procedure under the stated transformations. It also shows implementation simplifying a theoretical pipeline. Normal forms are not sacred; they are interfaces chosen to make subsequent operations feasible.

Encoding affects auditability. An octal atom identifier is efficient for tables but not self-explanatory. Cross-reference lists must remain consistent with the conjunction table, polarity counts and ready list. A corrupted pointer can make a valid logical rule operate on the wrong occurrences. Machine correctness therefore includes representation invariants absent from a pencil proof.

The sum is called the tuple's norm. Enumerating every positive integer tuple by increasing norm is fair: any required finite tuple eventually arrives. The particular order among equal-norm tuples affects when a contradiction becomes visible but not whether it is eventually reached in unbounded time and storage.

The fragile part is term naming. Substituting early tuples can expose new function terms; the program numbers those “constants” in order of appearance. Rearranging clauses in the input changes that discovery order. The same semantic formula can therefore assign different integer ranks to key terms, moving a necessary tuple much earlier or later in the enumeration.

The paper reports a valid formula expressing that uniform continuity implies continuity. Simply shuffling the punched-data deck changed the number of required quantifier-free lines by a factor of ten, from roughly 500 to 5,000. In some orderings the program could prove it before exhausting fast storage; in others it could not.

This is a profound distinction between fairness and feasibility. Both schedules eventually reach every term in an ideal unbounded run. Only one may reach the decisive instance within actual capacity. Completeness is invariant to fair reordering; operational success is not. A machine prover needs relevance and ordering heuristics as surely as it needs sound inference rules.

The conjunction table stores one machine word per literal occurrence. It is the clause-level image of the QFL conjunction. The formula table has one entry per atom; each entry heads two linked lists, one for positive occurrences and one for negative occurrences in the conjunction table.

Each formula-table entry also records the number of clauses containing each polarity and the total number of literals in those clauses. The formula table itself is a two-way linked list. A third, short ready list contains atoms to which the one-literal rule or affirmative-negative rule applies.

These redundant views turn global questions into local updates. Purity can be detected from a zero polarity count. A unit clause can place its literal on the ready list. Deleting a clause follows occurrence links rather than searching every word. The cost is a web of consistency obligations: every mutation must update links, counts and readiness together.

The paper reduces all processing rules to two basic operations. One routine deletes occurrences of a literal from QFL clauses; another eliminates all clauses containing a chosen literal. Deletion can create new unit clauses. Clause elimination can make an atom pure. The ready list directs the machine to consequences created by the previous operation until no cheap reduction remains.

If both p and ¬p are about to enter the ready list as units, inconsistency has been found. Otherwise a ready entry triggers deletion and clause elimination, whose updates may create more units or pure atoms. The machine follows that chain to a fixed point.

For Rule III*, the authors used the first entry in the formula table as the split atom and did not systematically test competing heuristics. They explicitly note that the choice may be critical to computation length. A poor decision can hide short propagation cascades and double large subproblems; a good one can expose a conflict immediately.

The program's discipline resembles what is now called Boolean constraint propagation followed by a decision. Yet the 1962 text has its own implementation vocabulary and does not include later watched literals, non-chronological backtracking or learned clauses. Calling all those features “DPLL” risks replacing the paper's actual machine with its descendants.

The deeper principle is that control state should distinguish inference from speculation. Ready-list operations are justified by the current formula and do not need an alternative branch. A split adds a hypothesis and therefore must preserve the road not taken. Backtracking is not error correction; it is the planned completion of a logically exhaustive case division.

A predicate-calculus formula on which Gilmore's program had been halted after about 21 minutes and seven substitutions was proved by the new program in under two minutes. The DPLL machine generated about 60 quantifier-free lines before inconsistency appeared. The earlier 1960 hand calculation had found inconsistency at 25 lines; the discrepancy came from a different constant-generation rule.

The uniform-continuity-implies-continuity formula required more than 500 lines and was proved in just over two minutes. The run nearly filled the machine to its planned capacity by generating 2,000 lines before applying reductions. That scheduling choice amortised processing but raised peak storage.

The program used a 32,768-word core and was coded in SAP with time-saving devices. The authors summarise its practical gain as a capacity of roughly 1,000 or 2,000 quantifier-free lines compared with a previous limit of 10 or 20. Additional line generation took time independent of how many lines already existed, but the number of lines needed grew extremely non-linearly with harder problems.

These measurements are historical observations on particular inputs and implementations. They do not establish an architecture-independent performance law. They do show why the paper's design decisions mattered: a split-and-stack Processor could make a 60-line contradiction usable where a resolution-expanding representation could not.

The authors avoid adding equality axioms by introducing a ternary predicate P(x,y,z), interpreted as x·y=z. They encode identity, inverse and associativity conditions, negate the desired conclusion and replace its existential with a constant s. Seven ground clauses suffice for a unit-reduction contradiction once the right substitutions have been generated.

The obstacle is not length of the final propositional refutation. It is reaching the decisive six-tuple of terms. Under the chosen increasing-sum enumeration, at least 3,003 lines must be generated and inconsistency appears by 5,005. The program could hold about 1,300 lines in the reported run.

The authors estimate that moving more tables to tape might increase capacity fourfold, just enough for that formulation. But place the conclusion before the axioms: without changing logical validity: and term numbering changes so the stated upper bound becomes 8,008 lines, beyond the projected machine. Other formulations are described as still less approachable.

This analysis shifts attention from deduction to relevance. The required clauses are easy to reduce after arrival; the generator spends its budget on thousands of irrelevant or premature instances. The paper closes by arguing that the most fruitful future work should reduce the number of QFLs considered by excluding irrelevant lines rather than merely expanding storage.

Modern DPLL is usually presented as a recursive SAT procedure: simplify units, remove pure literals, choose a variable, recurse under one value and then the other. The 1962 program embeds that propositional engine inside a first-order QFL generator. Its explicit machine implementation uses linked tables in core and a branch stack on tape.

GRASP in 1996 made conflict analysis and non-chronological backtracking central to SAT search. Chaff in 2001 combined careful Boolean-constraint-propagation engineering with a low-overhead decision strategy. Conflict-driven clause-learning solvers turn a failed branch into a reusable clause that prevents repetition. These are genuine extensions, not alternative descriptions of the tape stack.

The paper's split rule can generate new units, but it does not derive an asserting learned clause from an implication graph. Its backtracking is chronological because the LIFO tape restores the most recent untried branch. It has no watched-literal scheme, activity score or restart policy. Fidelity requires keeping the original state machine visible beneath the family name.

What persists is the control decomposition: maintain a clause state; exhaust forced consequences; make one speculative choice; preserve its alternative; detect conflict; retreat; certify failure only when no alternatives remain. That decomposition is durable because it separates logical necessity from search policy.

Review one: scholarship. Every quantitative claim is anchored in the four-page primary: 32,768 core words, about 60 lines and under two minutes, more than 500 lines and just over two minutes, 2,000 generated lines before reduction, the 3,003–5,005 group-theorem window, about 1,300 achieved lines, the fourfold tape estimate and the 8,008 reordered bound. The account retains the authors' own disappointment and does not inflate a few trials into a universal benchmark.

Review two: teaching and execution. The split proof, LIFO control, QFL order and linked-table invariants each receive a worked example and a counterfactual probe. Ten SVG figures have unique accessible titles and descriptions; reduced-motion preference disables animation; colour is reinforced by labels; tables scroll on small screens. The laboratory checks 1,024 formulas against independent exhaustive evaluation, validates returned models and audits branch-stack accounting.

AI-telltale and evidence review. The prose avoids fabricated dialogue, quotation and claims that the machine “understood” its proofs. Later labels such as DPLL and CDCL are dated and separated from 1962 mechanisms. Military research sponsorship is reported only where relevant to the source record, never used as evidence for mathematical or political conclusions.

Scope review. The machine followed a fixed logical objective over encoded formulas. It did not choose goals, learn relevance from experience or establish anything about consciousness. Its formal-agency value lies in explicit control state: necessary consequences, speculative action, deferred alternative, conflict and return.

A split is an action under uncertainty about which Boolean commitment will work. The machine acts on one value, but correctness requires preserving the alternative. Tape is therefore not passive storage; it is the material form of an unfulfilled logical obligation.

The ready list marks actions that are no longer choices. A unit clause fixes a value; a pure literal supplies a harmless one. Only an empty ready list authorises speculation. This separation between forced and optional moves is one reason the architecture remains legible across later SAT systems.

The failed group example adds a second lesson. Perfect backtracking over the current clauses cannot help if decisive clauses have not been generated. Search control operates at two scales: which ground evidence to instantiate and which Boolean branch to explore. Optimising one layer can expose the other as the dominant bottleneck.

For formal agency, the durable pattern is bounded commitment. Make a reversible choice, retain enough state to undo it, propagate consequences, and recognise the exact condition under which alternatives are exhausted. This is not consciousness. It is a precise account of how a machine can pursue a symbolic goal without confusing one failed path with global failure.