Directory /walsh/code/Results

Results are organized into 3 folders, one for each logical system: C0, C1, and CN.

Each folder contains:
A file "C?_??_Full.txt" this is the direct output of the GenerateTautologyFile function with appropriate parameters. For example, "CN21Results/CN_21_Full.txt" is generated by running: GenerateTautologyFile(21, "CN_21_OUTPUT", "CN")
A file "C?_??_CounterModels.txt" this file contains the same list as "C?_??_Full.txt" but each line may or may not contain a countermodel. If the line does contain a countermodel it will look like: "[POLISH]:[COUNTERMODEL STRING]". Countermodel strings can be decoded with Models.model_from_string().
A subfolder named specialcases.

The special cases folder contains:
A file "C?_??_Remaining.txt" that contains all lines from "C?_??_CounterModels.txt" that don't have a countermodel.
Additionally it may contain files with the name "[POLISH].out" that are output files from vampire that prove that formula that is in the name of the file is not a single axiom. This is not restricted to countermodels.