#!/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
#	bird1.desc
#	bird1.ver1.clauses
#	bird1.ver1.in
#	bird1.ver1.out
#	bird2.desc
#	bird2.ver1.clauses
#	bird2.ver1.in
#	bird2.ver1.out
#	bird4.desc
#	bird4.ver1.clauses
#	bird4.ver1.in
#	bird4.ver1.out
#	bird4.ver2.clauses
#	bird4.ver2.in
#	bird4.ver2.out
#	bird5.desc
#	bird5.ver1.clauses
#	bird5.ver1.in
#	bird5.ver1.out
#	bird6.desc
#	bird6.ver1.clauses
#	bird6.ver1.in
#	bird6.ver1.out
#	bird7.desc
#	bird7.ver1.clauses
#	bird7.ver1.in
#	bird7.ver1.out
#	bird8.desc
#	bird8.ver1.clauses
#	bird8.ver1.in
#	bird8.ver1.out
# This archive created: Tue Aug 16 11:22:14 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/puzzles/birds/README
created: 07/26/88
revised: 07/26/88

Contents of 'birds' :
---------------------

These files that begin with 'bird' are the input files used by the
OTTER program to solve the problems in chapter 9 of TO MOCK A
MOCKING BIRD by Raymond Smullyan.  The number following the word
'bird' is the problem number. Above each clause in the files is
an informal derivation.   The following symbols are used:
	FA  -  for all
	TE  -  there exists
	-   -  not
	|   -  or
	and -  and

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

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

bird1 : 'The Significance of the Mockingbird'.  Hypothesis: Every bird is 
	fond of at least one other bird.        

bird2 : 'Egocentric?'.  Hypothesis: There exists a bird x that is fond of 
	itself.  

bird4 : 'A Question on Agreeable Birds'.  Hypothesis: If C is agreeable 
	then A is agreeable.

bird5 : 'An Exercise in Composition'.  Hypothesis: For all birds x, y, and 
	z, there exists a bird u such that for all w, uw = x(y(zw)).

bird6 : 'Compatible Birds'.  Hypothesis: Any two birds are compatible.

bird7 : 'Happy Birds'.  Hypothesis: Any bird that is fond of at least one 
	bird must be happy.

bird8 : 'Normal Birds'.  Hypothesis: If there exists a happy bird then there 
	exists a normal bird.


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

For each problem, there are several standard files, which include one
probname.desc file and at least one of each of probname.ver#,
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#, 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#
	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#    [ > 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
if test -f 'bird1.desc'
then
	echo shar: over-writing existing file "'bird1.desc'"
fi
cat << \SHAR_EOF > 'bird1.desc'
problem-set/puzzles/birds/bird1.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'The Significance of the Mockingbird'.
There exists a mocking bird (Mock).  For all birds x and y, there exists 
a bird z that composes x with y for all birds w.
Hypothesis: Every bird is fond of at least one other bird.        

Versions: 

bird1.ver1 : uses paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird1.ver1.clauses'
then
	echo shar: over-writing existing file "'bird1.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird1.ver1.clauses'
% problem-set/puzzles/birds/bird1.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 1, 
% 'The Significance of the Mockingbird'.

% representation:
%
% There exists a mocking bird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).
 
% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).
 

% Hypothesis: Every bird is fond of at least one other bird.        
% Finding clause:
%    -FAx TEy [response(x,y) = y].
%    TEx FAy -[response(x,y) = y].
%    Letting A = x,
%    -[response(A,y) = y]. 
% Denial clause:

-EQUAL(response(A,y),y).
SHAR_EOF
if test -f 'bird1.ver1.in'
then
	echo shar: over-writing existing file "'bird1.ver1.in'"
fi
cat << \SHAR_EOF > 'bird1.ver1.in'
% problem-set/puzzles/birds/bird1.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 1, 
% 'The Significance of the Mockingbird'.
% There exists a mocking bird (Mock).  For all birds x and y, there exists 
% a bird z that composes x with y for all birds w.
% Hypothesis: Every bird is fond of at least one other bird.        

% representation:
%

set(para_from).          
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).                                       

% There exists a mocking bird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).
 
% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).
 
end_of_list. 


list(sos).

% Hypothesis: Every bird is fond of at least one other bird.        
% Finding clause:
%    -FAx TEy [response(x,y) = y].
%    TEx FAy -[response(x,y) = y].
%    Letting A = x,
%    -[response(A,y) = y]. 
% Denial clause:

-EQUAL(response(A,y),y).

end_of_list.
SHAR_EOF
if test -f 'bird1.ver1.out'
then
	echo shar: over-writing existing file "'bird1.ver1.out'"
fi
cat << \SHAR_EOF > 'bird1.ver1.out'
problem-set/puzzles/birds/bird1.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(response(Mock,y),response(y,y)).
2 EQUAL(x,x).
3 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
end_of_list.

list(sos).
4 -EQUAL(response(A,y),y).
end_of_list.

---------------- PROOF ----------------

1 EQUAL(response(Mock,y),response(y,y)).
2 EQUAL(x,x).
3 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
4 -EQUAL(response(A,y),y).
5 (3,4) -EQUAL(response(comp(A,x),y),response(x,y)).
8 (1,5) -EQUAL(response(Mock,comp(A,x)),response(x,comp(A,x))).
13 (8,2) .

--------------- options ---------------
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  4
clauses given                  3
clauses generated             11
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed       2
(clauses subsumed by sos)      0
unit deletions                 0
clauses kept                   9
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          0

----------- times (seconds) -----------
run time             0.29
input time           0.08
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.00
para_into time       0.02
para_from time       0.00
pre_process time     0.07
  demod time         0.00
  weigh time         0.00
  for_sub time       0.00
  unit_del time      0.00
post_process time    0.01
  back_sub time      0.00
  conflict time      0.01
  factor time        0.00
FPA build time       0.03
IS build time        0.01
print_cl time        0.05
cl integrate time    0.01
window time          0.00
SHAR_EOF
if test -f 'bird2.desc'
then
	echo shar: over-writing existing file "'bird2.desc'"
fi
cat << \SHAR_EOF > 'bird2.desc'
problem-set/puzzles/birds/bird2.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'Egocentric?'.
There exists a mocking bird (Mock).  For all birds x and y, there exists 
a bird z that composes x with y for all birds w.
Hypothesis: There exists a bird x that is fond of itself.  

Versions: 

bird2.ver1 : uses paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird2.ver1.clauses'
then
	echo shar: over-writing existing file "'bird2.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird2.ver1.clauses'
% problem-set/puzzles/birds/bird2.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 2,
% 'Egocentric?'.

% representation:
%

% There exists a mocking bird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).


% Hypothesis: There exists a bird x that is fond of itself.  
% Finding clause:
%    -TEx [response(x,x) = x].
%    FAx -[response(x,x) = x].
% Denial clause:

-EQUAL(response(x,x),x) | $ans(x).
SHAR_EOF
if test -f 'bird2.ver1.in'
then
	echo shar: over-writing existing file "'bird2.ver1.in'"
fi
cat << \SHAR_EOF > 'bird2.ver1.in'
% problem-set/puzzles/birds/bird2.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 2,
% 'Egocentric?'.
% There exists a mocking bird (Mock).  For all birds x and y, there exists 
% a bird z that composes x with y for all birds w.
% Hypothesis: There exists a bird x that is fond of itself.  

% representation:
%

set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).                                          

% There exists a mocking bird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

end_of_list.


list(sos).                                               

% Hypothesis: There exists a bird x that is fond of itself.  
% Finding clause:
%    -TEx [response(x,x) = x].
%    FAx -[response(x,x) = x].
% Denial clause:

-EQUAL(response(x,x),x) | $ans(x).

end_of_list.
SHAR_EOF
if test -f 'bird2.ver1.out'
then
	echo shar: over-writing existing file "'bird2.ver1.out'"
fi
cat << \SHAR_EOF > 'bird2.ver1.out'
problem-set/puzzles/birds/bird2.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(response(Mock,y),response(y,y)).
2 EQUAL(x,x).
3 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
end_of_list.

list(sos).
4 -EQUAL(response(x,x),x) | $ans(x).
end_of_list.

---------------- PROOF ----------------

1 EQUAL(response(Mock,y),response(y,y)).
2 EQUAL(x,x).
3 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
4 -EQUAL(response(x,x),x) | $ans(x).
7 (1,4) -EQUAL(response(Mock,x),x) | $ans(x).
8 (3,7) -EQUAL(response(comp(Mock,x),y),response(x,y)) | $ans(response(x,y)).
10 (1,8) -EQUAL(response(Mock,comp(Mock,x)),response(x,comp(Mock,x))) | $ans(response(x,comp(Mock,x))).
15 (10,2) $ans(response(Mock,comp(Mock,Mock))).

--------------- options ---------------
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  4
clauses given                  3
clauses generated             15
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed       4
(clauses subsumed by sos)      0
unit deletions                 0
clauses kept                  11
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          7

----------- times (seconds) -----------
run time             0.38
input time           0.08
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.00
para_into time       0.03
para_from time       0.00
pre_process time     0.12
  demod time         0.00
  weigh time         0.00
  for_sub time       0.01
  unit_del time      0.00
post_process time    0.02
  back_sub time      0.00
  conflict time      0.01
  factor time        0.00
FPA build time       0.03
IS build time        0.01
print_cl time        0.09
cl integrate time    0.02
window time          0.00
SHAR_EOF
if test -f 'bird4.desc'
then
	echo shar: over-writing existing file "'bird4.desc'"
fi
cat << \SHAR_EOF > 'bird4.desc'
problem-set/puzzles/birds/bird4.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'A Question on Agreeable Birds'.
For all birds x and y, there exists a bird z that composes x with y for all 
birds w.
Hypothesis: If C is agreeable then A is agreeable.

Versions: 

bird4.ver1 : uses paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88

bird4.ver2 : uses UR resolution and paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird4.ver1.clauses'
then
	echo shar: over-writing existing file "'bird4.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird4.ver1.clauses'
% problem-set/puzzles/birds/bird4.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 4,
% 'A Question on Agreeable Birds'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,j
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Hypothesis: If C is agreeable then A is agreeable.
% Finding clause:
%    -[ If FAx TEy (response(C,y) = response(x,y)),
%       then FAw TEv (response(A,v) = response(w,v)) ].
%    -[ TEx FAy -(response(C,y) = response(x,y)) |
%       FAw TEv (response(A,v) = response(w,v)) ].
%    FAx TEy (response(C,y) = response(x,y)) and
%       TEw FAv -(response(A,v) = response(w,v).
%    Letting common_bird(x) = y and odd_bird = w,
%    response(C,commom_bird(x)) = response(x,common_bird(x)) and
%       -(response(A,v) = response(odd_bird,v)).
% Denial clause:

EQUAL(response(C,common_bird(x)),response(x,common_bird(x))).
-EQUAL(response(A,v),response(odd_bird,v)).

% C composes A with B.
% Clause:

EQUAL(C,comp(A,B)).
SHAR_EOF
if test -f 'bird4.ver1.in'
then
	echo shar: over-writing existing file "'bird4.ver1.in'"
fi
cat << \SHAR_EOF > 'bird4.ver1.in'
% problem-set/puzzles/birds/bird4.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 4,
% 'A Question on Agreeable Birds'.
% For all birds x and y, there exists a bird z that composes x with y for all 
% birds w.
% Hypothesis: If C is agreeable then A is agreeable.

% representation:
%

set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).                                              

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,j
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

end_of_list.


list(sos).

% Hypothesis: If C is agreeable then A is agreeable.
% Finding clause:
%    -[ If FAx TEy (response(C,y) = response(x,y)),
%       then FAw TEv (response(A,v) = response(w,v)) ].
%    -[ TEx FAy -(response(C,y) = response(x,y)) |
%       FAw TEv (response(A,v) = response(w,v)) ].
%    FAx TEy (response(C,y) = response(x,y)) and
%       TEw FAv -(response(A,v) = response(w,v).
%    Letting common_bird(x) = y and odd_bird = w,
%    response(C,commom_bird(x)) = response(x,common_bird(x)) and
%       -(response(A,v) = response(odd_bird,v)).
% Denial clause:

EQUAL(response(C,common_bird(x)),response(x,common_bird(x))).
-EQUAL(response(A,v),response(odd_bird,v)).

% C composes A with B.
% Clause:

EQUAL(C,comp(A,B)).

end_of_list.
SHAR_EOF
if test -f 'bird4.ver1.out'
then
	echo shar: over-writing existing file "'bird4.ver1.out'"
fi
cat << \SHAR_EOF > 'bird4.ver1.out'
problem-set/puzzles/birds/bird4.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(x,x).
2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
end_of_list.

list(sos).
3 EQUAL(response(C,common_bird(x)),response(x,common_bird(x))).
4 -EQUAL(response(A,v),response(odd_bird,v)).
5 EQUAL(C,comp(A,B)).
end_of_list.

---------------- PROOF ----------------

2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
3 EQUAL(response(C,common_bird(x)),response(x,common_bird(x))).
4 -EQUAL(response(A,v),response(odd_bird,v)).
5 EQUAL(C,comp(A,B)).
6 (5,2) EQUAL(response(C,x),response(A,response(B,x))).
8 (2,4) -EQUAL(response(A,response(x,y)),response(comp(odd_bird,x),y)).
20 (6,3) EQUAL(response(A,response(B,common_bird(x))),response(x,common_bird(x))).
25 (20,8) .

--------------- options ---------------
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  5
clauses given                  4
clauses generated             41
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed      21
(clauses subsumed by sos)      3
unit deletions                 0
clauses kept                  20
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          6

----------- times (seconds) -----------
run time             0.56
input time           0.09
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.00
para_into time       0.03
para_from time       0.04
pre_process time     0.21
  demod time         0.00
  weigh time         0.01
  for_sub time       0.03
  unit_del time      0.00
post_process time    0.05
  back_sub time      0.02
  conflict time      0.02
  factor time        0.00
FPA build time       0.05
IS build time        0.02
print_cl time        0.11
cl integrate time    0.03
window time          0.00
SHAR_EOF
if test -f 'bird4.ver2.clauses'
then
	echo shar: over-writing existing file "'bird4.ver2.clauses'"
fi
cat << \SHAR_EOF > 'bird4.ver2.clauses'
% problem-set/puzzles/birds/bird4.ver2.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 4,
% 'A Question on Agreeable Birds'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,j
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Definition of agreeable: A bird x is agreeable if and only if
% for all birds y there exists a bird z such that xz = yz.
% Finding clause:
%   1) If agreeable(x) then FAy TEz [response(x,z) = response(y,z)] and
%   2) if TEx FAy TEz [response(x,z) = response(y,z)] then agreeable(x).
%   1) Letting commom_bird(y) = z,
%      -agreeable(x) | 
%         response(x,common_bird(y)) = response(y,common_bird(y)).
%   2) FAx TEy FAz -[response(x,z) = response(y,z)] | agreeable(x).
%      Letting compatible(x) = y,
%      -[response(x,z) = response(compatible(x),z)] | agreeable(x).
% Clause 1:

-agreeable(x) |
EQUAL(response(x,common_bird(y)),response(y,common_bird(y))).

% Clause 2:

-EQUAL(response(x,z),response(compatible(x),z)) | agreeable(x).
 

% Hypothesis: If C is agreeable then A is agreeable.
% Finding clause:
%    - [ If agreeable(C) then agreeable(A) ].
%    - [ -agreeable(C) | agreeable(A) ].
%    agreeable(C) and -agreeable(A).
% Denial clause:

agreeable(C).
-agreeable(A).

% C composes A with B.
% Clause:

EQUAL(C,comp(A,B)).
SHAR_EOF
if test -f 'bird4.ver2.in'
then
	echo shar: over-writing existing file "'bird4.ver2.in'"
fi
cat << \SHAR_EOF > 'bird4.ver2.in'
% problem-set/puzzles/birds/bird4.ver2.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 4,
% 'A Question on Agreeable Birds'.
% For all birds x and y, there exists a bird z that composes x with y for all 
% birds w.
% Hypothesis: If C is agreeable then A is agreeable.

% representation:
%

set(UR_res).
set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms). 

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,j
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Definition of agreeable: A bird x is agreeable if and only if
% for all birds y there exists a bird z such that xz = yz.
% Finding clause:
%   1) If agreeable(x) then FAy TEz [response(x,z) = response(y,z)] and
%   2) if TEx FAy TEz [response(x,z) = response(y,z)] then agreeable(x).
%   1) Letting commom_bird(y) = z,
%      -agreeable(x) | 
%         response(x,common_bird(y)) = response(y,common_bird(y)).
%   2) FAx TEy FAz -[response(x,z) = response(y,z)] | agreeable(x).
%      Letting compatible(x) = y,
%      -[response(x,z) = response(compatible(x),z)] | agreeable(x).
% Clause 1:

-agreeable(x) |
EQUAL(response(x,common_bird(y)),response(y,common_bird(y))).

% Clause 2:

-EQUAL(response(x,z),response(compatible(x),z)) | agreeable(x).
 
end_of_list.


list(sos).

% Hypothesis: If C is agreeable then A is agreeable.
% Finding clause:
%    - [ If agreeable(C) then agreeable(A) ].
%    - [ -agreeable(C) | agreeable(A) ].
%    agreeable(C) and -agreeable(A).
% Denial clause:

agreeable(C).
-agreeable(A).

% C composes A with B.
% Clause:

EQUAL(C,comp(A,B)).

end_of_list.
SHAR_EOF
if test -f 'bird4.ver2.out'
then
	echo shar: over-writing existing file "'bird4.ver2.out'"
fi
cat << \SHAR_EOF > 'bird4.ver2.out'
problem-set/puzzles/birds/bird4.ver2.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(UR_res).
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(x,x).
2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
3 -agreeable(x) | EQUAL(response(x,common_bird(y)),response(y,common_bird(y))).
4 -EQUAL(response(x,z),response(compatible(x),z)) | agreeable(x).
end_of_list.

list(sos).
5 agreeable(C).
6 -agreeable(A).
7 EQUAL(C,comp(A,B)).
end_of_list.

---------------- PROOF ----------------

2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
3 -agreeable(x) | EQUAL(response(x,common_bird(y)),response(y,common_bird(y))).
4 -EQUAL(response(x,z),response(compatible(x),z)) | agreeable(x).
5 agreeable(C).
6 -agreeable(A).
7 EQUAL(C,comp(A,B)).
8 (5,3) EQUAL(response(C,common_bird(x)),response(x,common_bird(x))).
9 (6,4) -EQUAL(response(A,x),response(compatible(A),x)).
11 (7,2) EQUAL(response(C,x),response(A,response(B,x))).
17 (2,9) -EQUAL(response(A,response(x,y)),response(comp(compatible(A),x),y)).
35 (11,8) EQUAL(response(A,response(B,common_bird(x))),response(x,common_bird(x))).
40 (35,17) .

--------------- options ---------------
set(UR_res).
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  7
clauses given                  7
clauses generated             71
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed      38
(clauses subsumed by sos)      9
unit deletions                 0
clauses kept                  33
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          6

----------- times (seconds) -----------
run time             0.86
input time           0.12
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.01
para_into time       0.05
para_from time       0.05
pre_process time     0.36
  demod time         0.00
  weigh time         0.01
  for_sub time       0.07
  unit_del time      0.00
post_process time    0.08
  back_sub time      0.03
  conflict time      0.04
  factor time        0.00
FPA build time       0.08
IS build time        0.03
print_cl time        0.17
cl integrate time    0.04
window time          0.00
SHAR_EOF
if test -f 'bird5.desc'
then
	echo shar: over-writing existing file "'bird5.desc'"
fi
cat << \SHAR_EOF > 'bird5.desc'
problem-set/puzzles/birds/bird5.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'An Exercise in Composition'.
For all birds x and y, there exists a bird z that composes x with y for all 
birds w.  Hypothesis: For all birds x, y, and z, there exists a bird u such 
that for all w, uw = x(y(zw)).

Versions: 

bird5.ver1 : uses paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird5.ver1.clauses'
then
	echo shar: over-writing existing file "'bird5.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird5.ver1.clauses'
% problem-set/puzzles/birds/bird5.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 5,
% 'An Exercise in Composition'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Hypothesis: For all birds x, y, and z, there exists a bird u such 
% that for all w, uw = x(y(zw)).
% Finding clause (using xy to replace response(x,y) for compactness):
%   - (FAx FAy FAz TEu FAw (uw = x(y(zw)))).
%   TEx TEy TEz FAu TEw -(uw = x(y(zw))).
%   Letting w = f(u), x = A, y = B, and z = C,
%   -[(u)f(u) = A(B((C)f(u)))].
% Denial clause:

-EQUAL(response(u,f(u)),response(A,response(B,response(C,f(u))))) |
   $ans(u).
SHAR_EOF
if test -f 'bird5.ver1.in'
then
	echo shar: over-writing existing file "'bird5.ver1.in'"
fi
cat << \SHAR_EOF > 'bird5.ver1.in'
% problem-set/puzzles/birds/bird5.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 5,
% 'An Exercise in Composition'.
% For all birds x and y, there exists a bird z that composes x with y for all 
% birds w.  Hypothesis: For all birds x, y, and z, there exists a bird u such 
% that for all w, uw = x(y(zw)).

% representation:
%

set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

end_of_list.


list(sos).

% Hypothesis: For all birds x, y, and z, there exists a bird u such 
% that for all w, uw = x(y(zw)).
% Finding clause (using xy to replace response(x,y) for compactness):
%   - (FAx FAy FAz TEu FAw (uw = x(y(zw)))).
%   TEx TEy TEz FAu TEw -(uw = x(y(zw))).
%   Letting w = f(u), x = A, y = B, and z = C,
%   -[(u)f(u) = A(B((C)f(u)))].
% Denial clause:

-EQUAL(response(u,f(u)),response(A,response(B,response(C,f(u))))) |
   $ans(u).

end_of_list.
SHAR_EOF
if test -f 'bird5.ver1.out'
then
	echo shar: over-writing existing file "'bird5.ver1.out'"
fi
cat << \SHAR_EOF > 'bird5.ver1.out'
problem-set/puzzles/birds/bird5.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(x,x).
2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
end_of_list.

list(sos).
3 -EQUAL(response(u,f(u)),response(A,response(B,response(C,f(u))))) | $ans(u).
end_of_list.

---------------- PROOF ----------------

2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
3 -EQUAL(response(u,f(u)),response(A,response(B,response(C,f(u))))) | $ans(u).
4 (2,3) -EQUAL(response(x,response(y,f(comp(x,y)))),response(A,response(B,response(C,f(comp(x,y)))))) | $ans(comp(x,y)).
7 (4,2) $ans(comp(comp(A,B),C)).

--------------- options ---------------
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  3
clauses given                  1
clauses generated              4
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed       0
(clauses subsumed by sos)      0
unit deletions                 0
clauses kept                   4
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          0

----------- times (seconds) -----------
run time             0.23
input time           0.07
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.00
para_into time       0.01
para_from time       0.00
pre_process time     0.03
  demod time         0.00
  weigh time         0.00
  for_sub time       0.00
  unit_del time      0.00
post_process time    0.01
  back_sub time      0.00
  conflict time      0.00
  factor time        0.00
FPA build time       0.02
IS build time        0.00
print_cl time        0.04
cl integrate time    0.01
window time          0.00
SHAR_EOF
if test -f 'bird6.desc'
then
	echo shar: over-writing existing file "'bird6.desc'"
fi
cat << \SHAR_EOF > 'bird6.desc'
problem-set/puzzles/birds/bird6.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'Compatible Birds'.
There exists a mockingbird (Mock).  For all birds x and y, there exists a 
bird z that composes x with y for all birds w.
Hypothesis: Any two birds are compatible.

Versions: 

bird6.ver1 : uses UR resolution and paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird6.ver1.clauses'
then
	echo shar: over-writing existing file "'bird6.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird6.ver1.clauses'
% problem-set/puzzles/birds/bird6.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 6, 
% 'Compatible Birds'.

% representation:
%

% There exists a mockingbird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Hypothesis: Any two birds are compatible.
% Finding clause (using xy to replace response(x,y) for compactness):
%    -FAx FAy TEw TEz [(xw = z) and (yz = w)].
%    TEx TEy FAw FAz -[(xw = z) and (yz = w)].
%    Letting A = x, B = y, x = w, and y = z,
%    -(Ax = y) | -(By = x).
% Denial clause:

-EQUAL(response(A,x),y) | -EQUAL(response(B,y),x).
SHAR_EOF
if test -f 'bird6.ver1.in'
then
	echo shar: over-writing existing file "'bird6.ver1.in'"
fi
cat << \SHAR_EOF > 'bird6.ver1.in'
% problem-set/puzzles/birds/bird6.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 6, 
% 'Compatible Birds'.
% There exists a mockingbird (Mock).  For all birds x and y, there exists a 
% bird z that composes x with y for all birds w.
% Hypothesis: Any two birds are compatible.

% representation:
%

set(UR_res).
set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).

% There exists a mockingbird (Mock).
% Finding clause:
%    TEx FAy [response(x,y) = response(y,y)].
%    Letting Mock = x,
%    response(Mock,y) = response(y,y).
% Clause:

EQUAL(response(Mock,y),response(y,y)).

% x is equal to x.
% Clause:

EQUAL(x,x).

% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

end_of_list.


list(sos).

% Hypothesis: Any two birds are compatible.
% Finding clause (using xy to replace response(x,y) for compactness):
%    -FAx FAy TEw TEz [(xw = z) and (yz = w)].
%    TEx TEy FAw FAz -[(xw = z) and (yz = w)].
%    Letting A = x, B = y, x = w, and y = z,
%    -(Ax = y) | -(By = x).
% Denial clause:

-EQUAL(response(A,x),y) | -EQUAL(response(B,y),x).

end_of_list.
SHAR_EOF
if test -f 'bird6.ver1.out'
then
	echo shar: over-writing existing file "'bird6.ver1.out'"
fi
cat << \SHAR_EOF > 'bird6.ver1.out'
problem-set/puzzles/birds/bird6.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(UR_res).
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(response(Mock,y),response(y,y)).
2 EQUAL(x,x).
3 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
end_of_list.

list(sos).
4 -EQUAL(response(A,x),y) | -EQUAL(response(B,y),x).
end_of_list.

---------------- PROOF ----------------

1 EQUAL(response(Mock,y),response(y,y)).
2 EQUAL(x,x).
3 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
4 -EQUAL(response(A,x),y) | -EQUAL(response(B,y),x).
5 (4,2) -EQUAL(response(A,response(B,x)),x).
13 (3,5) -EQUAL(response(comp(A,B),x),x).
18 (3,13) -EQUAL(response(comp(comp(A,B),x),y),response(x,y)).
41 (1,18) -EQUAL(response(Mock,comp(comp(A,B),x)),response(x,comp(comp(A,B),x))).
46 (41,2) .

--------------- options ---------------
set(UR_res).
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  4
clauses given                 17
clauses generated             62
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed      20
(clauses subsumed by sos)      1
unit deletions                 0
clauses kept                  42
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          7

----------- times (seconds) -----------
run time             0.97
input time           0.09
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.03
para_into time       0.11
para_from time       0.00
pre_process time     0.41
  demod time         0.00
  weigh time         0.02
  for_sub time       0.06
  unit_del time      0.00
post_process time    0.10
  back_sub time      0.04
  conflict time      0.05
  factor time        0.00
FPA build time       0.10
IS build time        0.03
print_cl time        0.22
cl integrate time    0.05
window time          0.00
SHAR_EOF
if test -f 'bird7.desc'
then
	echo shar: over-writing existing file "'bird7.desc'"
fi
cat << \SHAR_EOF > 'bird7.desc'
problem-set/puzzles/birds/bird7.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'Happy Birds'.
First part of denial clause: there exists a bird which is fond of some other 
bird. Hypothesis: Any bird that is fond of at least one bird must be happy.

Versions: 

bird7.ver1 : uses UR resolution and paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird7.ver1.clauses'
then
	echo shar: over-writing existing file "'bird7.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird7.ver1.clauses'
% problem-set/puzzles/birds/bird7.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 7, 
% 'Happy Birds'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).

% First part of denial clause: there exists a bird which is fond
% of some other bird. 

EQUAL(response(A,B),B).        

% Hypothesis: Any bird that is fond of at least one bird must be happy.
% Finding clause:
%   - FAx [If TEy (xy = y) then TEz TEw (xz = w) and (xw = z)].
%   TEx -[- TEy (xy = y) | TEz TEw ((xz = w) and (xw = z))].
%   TEx [ TEy (xy = y) and - TEz TEw ((xz = w) and (xw = z)) ].
%   TEx [ TEy (xy = y) and FAz FAw -((xz = w) and (xw = z)) ].
%   Letting A = x,
%   TEy (Ay = y) and FAz FAw -[(Az = w) and (Aw = z)].
%   Letting B = y,
%   (AB = B) and [-(Az = w) | -(Aw = z)].
% Denial clause:
%   Placing (AB = B) in the list of axiom, we have:

-EQUAL(response(A,z),w) | -EQUAL(response(A,w),z).
SHAR_EOF
if test -f 'bird7.ver1.in'
then
	echo shar: over-writing existing file "'bird7.ver1.in'"
fi
cat << \SHAR_EOF > 'bird7.ver1.in'
% problem-set/puzzles/birds/bird7.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 7, 
% 'Happy Birds'.
% First part of denial clause: there exists a bird which is fond of some other 
% bird. Hypothesis: Any bird that is fond of at least one bird must be happy.

% representation:
%

set(UR_res).
set(para_from).
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).

% x is equal to x.
% Clause:

EQUAL(x,x).

% First part of denial clause: there exists a bird which is fond
% of some other bird. 

EQUAL(response(A,B),B).        

end_of_list.


list(sos).  

% Hypothesis: Any bird that is fond of at least one bird must be happy.
% Finding clause:
%   - FAx [If TEy (xy = y) then TEz TEw (xz = w) and (xw = z)].
%   TEx -[- TEy (xy = y) | TEz TEw ((xz = w) and (xw = z))].
%   TEx [ TEy (xy = y) and - TEz TEw ((xz = w) and (xw = z)) ].
%   TEx [ TEy (xy = y) and FAz FAw -((xz = w) and (xw = z)) ].
%   Letting A = x,
%   TEy (Ay = y) and FAz FAw -[(Az = w) and (Aw = z)].
%   Letting B = y,
%   (AB = B) and [-(Az = w) | -(Aw = z)].
% Denial clause:
%   Placing (AB = B) in the list of axiom, we have:

-EQUAL(response(A,z),w) | -EQUAL(response(A,w),z).

end_of_list.
SHAR_EOF
if test -f 'bird7.ver1.out'
then
	echo shar: over-writing existing file "'bird7.ver1.out'"
fi
cat << \SHAR_EOF > 'bird7.ver1.out'
problem-set/puzzles/birds/bird7.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(UR_res).
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(x,x).
2 EQUAL(response(A,B),B).
end_of_list.

list(sos).
3 -EQUAL(response(A,z),w) | -EQUAL(response(A,w),z).
end_of_list.

---------------- PROOF ----------------

1 EQUAL(x,x).
2 EQUAL(response(A,B),B).
3 -EQUAL(response(A,z),w) | -EQUAL(response(A,w),z).
5 (2,3) -EQUAL(B,x) | -EQUAL(response(A,x),B).
6 (5,2) -EQUAL(B,B).
7 (6,1) .

--------------- options ---------------
set(UR_res).
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  3
clauses given                  3
clauses generated             10
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed       6
(clauses subsumed by sos)      2
unit deletions                 0
clauses kept                   4
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          0

----------- times (seconds) -----------
run time             0.22
input time           0.06
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.01
para_into time       0.00
para_from time       0.00
pre_process time     0.03
  demod time         0.00
  weigh time         0.00
  for_sub time       0.01
  unit_del time      0.00
post_process time    0.01
  back_sub time      0.00
  conflict time      0.00
  factor time        0.00
FPA build time       0.01
IS build time        0.00
print_cl time        0.03
cl integrate time    0.00
window time          0.00
SHAR_EOF
if test -f 'bird8.desc'
then
	echo shar: over-writing existing file "'bird8.desc'"
fi
cat << \SHAR_EOF > 'bird8.desc'
problem-set/puzzles/birds/bird8.desc
created : 08/11/88
revised : 08/16/88

Natural Language Description:
 
'Normal Birds'.
For all birds x and y, there exists a bird z that composes x with y for 
all birds w.
Hypothesis: If there exists a happy bird then there exists a normal bird.

Versions: 

bird8.ver1 : uses paramodulation with an equality formulation.

		created by : Shari McRae
		verified for ITP : untested
		translated for OTTER by : K.R.
		verified for OTTER : 06/28/88
SHAR_EOF
if test -f 'bird8.ver1.clauses'
then
	echo shar: over-writing existing file "'bird8.ver1.clauses'"
fi
cat << \SHAR_EOF > 'bird8.ver1.clauses'
% problem-set/puzzles/birds/bird8.ver1.clauses
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 8, 
% 'Normal Birds'.

% representation:
%

% x is equal to x.
% Clause:

EQUAL(x,x).
 
% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).

% Hypothesis: If there exists a happy bird then there exists 
% a normal bird.
% Finding clause (using xy to replace response(x,y) for compactness):
%    -[ If TEx TEy TEz (xy = z) and (xz = y)
%       then TEw TEv (wv = v) ].
%    -[ FAx FAy FAz -((xy = z) and (xz = y)) | TEw TEv (wv = v) ].
%    TEx TEy TEz [(xy = z) and (xz = y)] and FAw FAv -(wv = v).
%    Letting A = x, B = y, and C = z,
%    (AB = C) and (AC = B) and -(wv = v).
% Denial clause:

EQUAL(response(A,B),C).
EQUAL(response(A,C),B).
-EQUAL(response(w,v),v).
SHAR_EOF
if test -f 'bird8.ver1.in'
then
	echo shar: over-writing existing file "'bird8.ver1.in'"
fi
cat << \SHAR_EOF > 'bird8.ver1.in'
% problem-set/puzzles/birds/bird8.ver1.in
% created : 06/28/88
% revised : 08/11/88

% description:
%
% This is an input file for Chapter 9 problem 8, 
% 'Normal Birds'.
% For all birds x and y, there exists a bird z that composes x with y for 
% all birds w.
% Hypothesis: If there exists a happy bird then there exists a normal bird.

% representation:
%

set(para_from).          
set(para_into).
set(para_from_left). 
set(para_from_right).


list(axioms).                                       

% x is equal to x.
% Clause:

EQUAL(x,x).
 
% For all birds x and y, there exists a bird z that composes 
% x with y for all birds w.
% Finding clause:
%    FAx FAy TEz FAw [response(z,w) = response(x,response(y,w))].
%    Letting comp(x,y) = z,
%    response(comp(x,y),w) = response(x,response(y,w)).
% Clause:

EQUAL(response(comp(x,y),w),response(x,response(y,w))).
 
end_of_list. 


list(sos).

% Hypothesis: If there exists a happy bird then there exists 
% a normal bird.
% Finding clause (using xy to replace response(x,y) for compactness):
%    -[ If TEx TEy TEz (xy = z) and (xz = y)
%       then TEw TEv (wv = v) ].
%    -[ FAx FAy FAz -((xy = z) and (xz = y)) | TEw TEv (wv = v) ].
%    TEx TEy TEz [(xy = z) and (xz = y)] and FAw FAv -(wv = v).
%    Letting A = x, B = y, and C = z,
%    (AB = C) and (AC = B) and -(wv = v).
% Denial clause:

EQUAL(response(A,B),C).
EQUAL(response(A,C),B).
-EQUAL(response(w,v),v).

end_of_list.
SHAR_EOF
if test -f 'bird8.ver1.out'
then
	echo shar: over-writing existing file "'bird8.ver1.out'"
fi
cat << \SHAR_EOF > 'bird8.ver1.out'
problem-set/puzzles/birds/bird8.ver1.out
created : 08/11/88
revised : 08/11/88

OTTER version 0.91, 14 June 1988.

set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).

list(axioms).
1 EQUAL(x,x).
2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
end_of_list.

list(sos).
3 EQUAL(response(A,B),C).
4 EQUAL(response(A,C),B).
5 -EQUAL(response(w,v),v).
end_of_list.

---------------- PROOF ----------------

2 EQUAL(response(comp(x,y),w),response(x,response(y,w))).
3 EQUAL(response(A,B),C).
4 EQUAL(response(A,C),B).
5 -EQUAL(response(w,v),v).
9 (4,3) EQUAL(response(A,response(A,C)),C).
13 (2,5) -EQUAL(response(x,response(y,z)),z).
14 (13,9) .

--------------- options ---------------
set(para_from).
set(para_into).
set(para_from_left).
set(para_from_right).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(binary_res).
clear(hyper_res).
clear(UR_res).
clear(demod_inf).
clear(para_into_vars).
clear(para_from_vars).
clear(para_all).
clear(para_ones_rule).
clear(no_para_into_left).
clear(no_para_into_right).
clear(demod_linear).
clear(print_gen).
clear(sort_literals).
clear(Unit_deletion).
clear(factor).
clear(print_weight).
clear(sos_fifo).
clear(bird_print).
clear(atom_wt_max_args).
clear(print_lists_at_end).
clear(free_all_mem).
clear(for_sub_fpa).
clear(no_fapl).
clear(no_fanl).
clear(order_eq).

assign(report, 0).
assign(max_seconds, 0).
assign(max_given, 0).
assign(max_kept, 0).
assign(max_gen, 0).
assign(max_mem, 0).
assign(max_weight, 0).
assign(max_literals, 0).
assign(fpa_literals, 3).
assign(fpa_terms, 3).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                  5
clauses given                  3
clauses generated             17
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed       8
(clauses subsumed by sos)      0
unit deletions                 0
clauses kept                   9
empty clauses                  1
factors generated              0
clauses back subsumed          0
clauses not processed          5

----------- times (seconds) -----------
run time             0.29
input time           0.08
binary_res time      0.00
hyper_res time       0.00
UR_res time          0.00
para_into time       0.01
para_from time       0.01
pre_process time     0.06
  demod time         0.00
  weigh time         0.00
  for_sub time       0.01
  unit_del time      0.00
post_process time    0.02
  back_sub time      0.01
  conflict time      0.01
  factor time        0.00
FPA build time       0.02
IS build time        0.01
print_cl time        0.04
cl integrate time    0.01
window time          0.00
SHAR_EOF
#	End of shell archive
exit 0