problem-set/puzzles/gen.test/README created : 07/26/88 revised : 07/26/88 Contents of 'gen.test' : ------------------------ Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/puzzles/gen.test. interns : To solve "The Interns Puzzle" ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a % and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in through OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background.