The paper discusses the programming of a theorem-proving algorithm for the IBM 704 computer at the Institute of Mathematical Sciences, New York University. The algorithm, which is an improvement over previous methods, consists of two parts: the QFL-Generator and the Processor. The QFL-Generator generates a propositional calculus formula in conjunctive normal form, while the Processor tests its consistency. The authors introduce and justify a new rule (Rule III*) for eliminating atomic formulas, which is more efficient than the previous Rule III due to its ability to avoid increasing the number and length of clauses rapidly. The program uses auxiliary tape storage for Rule III* and fast access storage for the rest of the process. The authors also describe the coding of the matrix and conjunction of quantifier-free lines into linked memory tables. The results show that the program can prove complex theorems efficiently, such as uniform continuity implying continuity, but it struggles with certain group theory problems, highlighting the need for further improvements in handling "irrelevant" quantifier-free lines.The paper discusses the programming of a theorem-proving algorithm for the IBM 704 computer at the Institute of Mathematical Sciences, New York University. The algorithm, which is an improvement over previous methods, consists of two parts: the QFL-Generator and the Processor. The QFL-Generator generates a propositional calculus formula in conjunctive normal form, while the Processor tests its consistency. The authors introduce and justify a new rule (Rule III*) for eliminating atomic formulas, which is more efficient than the previous Rule III due to its ability to avoid increasing the number and length of clauses rapidly. The program uses auxiliary tape storage for Rule III* and fast access storage for the rest of the process. The authors also describe the coding of the matrix and conjunction of quantifier-free lines into linked memory tables. The results show that the program can prove complex theorems efficiently, such as uniform continuity implying continuity, but it struggles with certain group theory problems, highlighting the need for further improvements in handling "irrelevant" quantifier-free lines.