Fair Isaac deals with large knowledge bases in a variety of their lines of business. They are developing an automated theorem prover in the natural deduction framework to build on these data sets. The scale of the proofs and their attendant search spaces make textual proof display and analysis of the prover’s operation unreasonable. Thus, the Clinic team has developed a visualization system which greatly eases development efforts. It provides a structured display of the theorem prover’s search space and a programmable command-line interface which gives the developer significantly more flexibility than a conventional debugger would allow.