The Davis-Putnam procedure with splitting
In a New York University report of 8 June 1961 Martin Davis, George Logemann and Donald Loveland described a program for the IBM 704 that tests formulas by the Davis-Putnam method of 1960, with one of its rules replaced by a splitting rule. A formula on which Gilmore's program had run for 21 minutes without a result, it proved in under two minutes.
Why it matters
Instead of expanding the formula further, the program split the problem into two smaller ones and dropped branches already inconsistent. Formulas beyond the previous program became a matter of minutes, and problems of hundreds of quantifier-free lines came within reach.
The program keeps Davis and Putnam's one-literal clause rule and their rule for literals of one sign only, and replaces the third rule by splitting: a formula is inconsistent if and only if both of its branches are. The statement that uniform continuity implies continuity, over 500 quantifier-free lines, was found valid in just over two minutes. The machine's memory was 32,768 words. What the record does not claim: the content of Davis and Putnam's 1960 paper itself or of the 1962 journal version, both behind the ACM paywall; Davis and Putnam's rules are given here as the 1961 report states them.