The group at Northern Illinois University expanded to include John McCharen and Steve Winker, and eventually Ewing Lusk. In order to facilitate the increased diversity of experiments that the larger group wanted to undertake, it as decided to restructure WOS1 into a toolkit of assembly-language subroutines, and rewrite the upper levels, including the closure algorithm, in PL/1. (IBM machines were still the primary computers, both at Argonne and NIU.) This led to a series of systems that lasted nearly seven years, named NIUTP1-NIUTP7.
The notion of a toolkit with which one could build theorem provers was introduced at this time and became another theme for later Argonne development. In this case the approach was used to build a series of systems incorporating ever more complex variations on the closure algorithm without changing the underlying data structures and inference functions. The ultimate system (NIUTP7) provided a set of user-definable theorem-proving ``environments'', each running a version of the closure algorithm with different controlling parameters, and a meta-language for controlling their interactions[30]. There was enough control, and there were enough built-in predicates, that it became possible to ``program'' the theorem prover to perform a number of symbolic computational tasks. With these systems Winker and Wos began the systematic attack on open problems[25,26,32,31] and the work on qualification and locking was done[10]. The systems of this era were all built on the closure approach, although the PL/1 layer made it possible to rapidly customize it in order to apply it in unorthodox ways.