This paper presents a machine program for theorem-proving in quantification theory, based on an improved algorithm described in [1]. The algorithm consists of two parts: the QFl-Generator, which generates a propositional calculus formula in conjunctive normal form (the "quantifier-free lines"), and the Processor, which tests the consistency of this formula. An inconsistent set of quantifier-free lines constitutes a proof of the original formula. The algorithm used in testing for consistency was modified from Rule III to Rule III*, which splits the formula into two parts and checks their consistency separately. This change was made to avoid the rapid increase in the number and length of clauses, which was problematic in computer memory. The program uses auxiliary tape storage for Rule III* and fast access storage for the rest of the processing. The QFl-Generator converts the input formula into a quantifier-free matrix in conjunctive normal form, using a one-to-one assembler to translate the matrix into octal numbers. The program generates n-tuples of positive integers in increasing norm order to substitute into the matrix, creating new constants. The constants are ordered based on the input data, and the order can significantly affect the number of lines needed to prove a formula. The program uses two tables to store the quantifier-free lines: a conjunction table and a formula table. The formula table is a two-way linked list that includes counts of the number of clauses in which each literal occurs. A ready list is used to apply the one-literal clause and affirmative-negative rules until the ready list is empty. The program was tested on various formulas, including a complex example involving uniform continuity and continuity. It successfully proved this formula in under two minutes, generating over 500 quantifier-free lines. However, the program failed to prove a simple group theory problem, which required a left inverse to be a right inverse. This failure was due to the order of constants generated, which affected the number of lines needed to prove the formula. The program's performance was limited by the capacity of fast access storage, and the authors suggested that using tape storage could increase the number of quantifier-free lines that could be processed before running time became prohibitive. The program's ability to handle a larger number of quantifier-free lines was demonstrated, but the exponential growth in the number of lines needed for more complex problems remains a challenge. The authors suggest that future improvements could focus on reducing the number of quantifier-free lines that need to be considered by excluding irrelevant lines.This paper presents a machine program for theorem-proving in quantification theory, based on an improved algorithm described in [1]. The algorithm consists of two parts: the QFl-Generator, which generates a propositional calculus formula in conjunctive normal form (the "quantifier-free lines"), and the Processor, which tests the consistency of this formula. An inconsistent set of quantifier-free lines constitutes a proof of the original formula. The algorithm used in testing for consistency was modified from Rule III to Rule III*, which splits the formula into two parts and checks their consistency separately. This change was made to avoid the rapid increase in the number and length of clauses, which was problematic in computer memory. The program uses auxiliary tape storage for Rule III* and fast access storage for the rest of the processing. The QFl-Generator converts the input formula into a quantifier-free matrix in conjunctive normal form, using a one-to-one assembler to translate the matrix into octal numbers. The program generates n-tuples of positive integers in increasing norm order to substitute into the matrix, creating new constants. The constants are ordered based on the input data, and the order can significantly affect the number of lines needed to prove a formula. The program uses two tables to store the quantifier-free lines: a conjunction table and a formula table. The formula table is a two-way linked list that includes counts of the number of clauses in which each literal occurs. A ready list is used to apply the one-literal clause and affirmative-negative rules until the ready list is empty. The program was tested on various formulas, including a complex example involving uniform continuity and continuity. It successfully proved this formula in under two minutes, generating over 500 quantifier-free lines. However, the program failed to prove a simple group theory problem, which required a left inverse to be a right inverse. This failure was due to the order of constants generated, which affected the number of lines needed to prove the formula. The program's performance was limited by the capacity of fast access storage, and the authors suggested that using tape storage could increase the number of quantifier-free lines that could be processed before running time became prohibitive. The program's ability to handle a larger number of quantifier-free lines was demonstrated, but the exponential growth in the number of lines needed for more complex problems remains a challenge. The authors suggest that future improvements could focus on reducing the number of quantifier-free lines that need to be considered by excluding irrelevant lines.