#!/bin/sh
# This is a shell archive, meaning:
# 1. Remove everything above the #!/bin/sh line.
# 2. Save the resulting text in a file.
# 3. Execute the file with /bin/sh (not csh) to create the files:
#	README
# This archive created: Tue Aug 16 11:14:37 1988
export PATH; PATH=/bin:$PATH
if test -f 'README'
then
	echo shar: over-writing existing file "'README'"
fi
cat << \SHAR_EOF > 'README'
problem-set/prog.verification/README
created : 08/15/88
revised : 08/15/88

Contents of 'prog.verification' :
---------------------------------

Main File Headings
----------------------------------------------------------------------

README : You are currently here; a description of all the files in
	the directory problem-set/prog.verification.



----------------------------------------------------------------------

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, credits for problem formulation, 
	and 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 %, preceding the clauses to which they
	refer, and that clauses terminate with periods.

probname.ver#.out : contains the output from running probname.ver#.in
	with 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.

SHAR_EOF
#	End of shell archive
exit 0