In the course of its execution Snark typically outputs a lot of information as well as a proof when it finds one. All this output can be overwhelming to the user, yet invaluable in understanding why the proofs succeeded or failed. To deal with all this output Specware redirects all the Snark output to log files. In our example above, which executed a proof in the file pruf.sw, Specware will create a subdirectory called Snark at the same level as pruf.sw. In that directory a log file called pruf.log will be created that contains all the Snark output. In this same directory a specware file called pruf.sw will also be generated that includes an expanded version of the original spec containing the theorem to be proved. The original spec needs to be expanded before being passed to Snark because the Snark's logic is different from Specware's, lacking polymorphism and higher-order functions.