#!/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
#	animals.desc
#	animals.ver1.clauses
#	animals.ver1.in
#	animals.ver1.out
#	boys.desc
#	boys.ver1.clauses
#	boys.ver1.in
#	boys.ver1.out
#	ggson.desc
#	ggson.ver1.clauses
#	ggson.ver1.in
#	ggson.ver1.out
#	letters.desc
#	letters.ver1.clauses
#	letters.ver1.in
#	letters.ver1.out
#	lizard.desc
#	lizard.ver1.clauses
#	lizard.ver1.in
#	lizard.ver1.out
#	pigs.desc
#	pigs.ver1.clauses
#	pigs.ver1.in
#	pigs.ver1.out
#	winds.desc
#	winds.ver1.clauses
#	winds.ver1.in
#	winds.ver1.out
# This archive created: Tue Aug 16 11:21:36 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/carroll/README
created: 07/26/88
revised: 07/26/88

Contents of 'carroll' :
-----------------------

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

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

animals : To solve "The Animals" by Lewis Carroll.

boys : To solve "The School Boys" by Lewis Carroll.

ggson : To solve "The Great-grandson Problem" by Lewis Carroll.

letters : To solve "The Letters Puzzle" by Lewis Carroll

lizard : To solve "The Animals" by Lewis Carroll

pigs : To solve "The Pigs and Balloons Puzzle" by Lewis Carroll

winds : To solve "The Winds and the Windows" by Lewis Carroll

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

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.

SHAR_EOF
if test -f 'animals.desc'
then
	echo shar: over-writing existing file "'animals.desc'"
fi
cat << \SHAR_EOF > 'animals.desc'
problem-set/puzzles/carroll/animals.desc
created : 07/09/86
revised : 07/05/88

Natural Language Description:

                        The Animals

     (1)  The only animals in this house are cats.
     (2)  Every animal is suitable for a pet, that loves  to
          gaze at the moon.
     (3)  When I detest an animal, I avoid it.
     (4)  No animals are carnivorous, unless they  prowl  at
          night.
     (5)  No cat fails to kill mice.
     (6)  No animals ever take to me,  except  what  are  in
          this house.
     (7)  Kangaroos are not suitable for pets.
     (8)  None but carnivora kill mice.
     (9)  I detest animals that do not take to me.
     (10) Animals that prowl at night always love to gaze at
          the moon.
     The problem is to prove that "I  always  avoid  a  kan-
     garoo".
                                         - Lewis Carroll


Versions:

animals.ver1.in : declarative representation.

			created by : E. Lusk 
			verified for ITP : 07/09/86
			translated for OTTER by : K.R. 
			verified for OTTER : 07/14/88
SHAR_EOF
if test -f 'animals.ver1.clauses'
then
	echo shar: over-writing existing file "'animals.ver1.clauses'"
fi
cat << \SHAR_EOF > 'animals.ver1.clauses'
% problem-set/puzzles/carroll/animals.ver1.clauses
% created : 07/14/88
% revised : 07/14/88

% description:
%
% This run solves a puzzle called "The Animals" by Lewis Carroll
% using UR-resolution.
%
%                       The Animals
%
%    (1)  The only animals in this house are cats.
%    (2)  Every animal is suitable for a pet, that loves  to
%         gaze at the moon.
%    (3)  When I detest an animal, I avoid it.
%    (4)  No animals are carnivorous, unless they  prowl  at
%         night.
%    (5)  No cat fails to kill mice.
%    (6)  No animals ever take to me,  except  what  are  in
%         this house.
%    (7)  Kangaroos are not suitable for pets.
%    (8)  None but carnivora kill mice.
%    (9)  I detest animals that do not take to me.
%    (10) Animals that prowl at night always love to gaze at
%         the moon.
%    The problem is to prove that "I  always  avoid  a  kan-
%    garoo".
%                                        - Lewis Carroll

% representation:
% 
% declare_predicates(1,[INHOUSE,CAT,GAZER,SUITABLEPET,DETESTED,AVOIDED])
% declare_predicates(1,[CARNIVORE,PROWLER,MOUSEKILLER,TAKESTOME,KANGAROO])
% declare_constant(f1).   
% declare_variable(x1).
%
% PREDICATES : CAT(x) = x is a cat.
%    INHOUSE(x) = x is an animal in the house.
%    SUITABLEPET= an animal suitable for a pet.
%    PROWLER= animals who prowl at night.

-INHOUSE(x1) | CAT(x1).
-GAZER(x1) | SUITABLEPET(x1).
-DETESTED(x1) | AVOIDED(x1). 
-CARNIVORE(x1) | PROWLER(x1).
-CAT(x1) | MOUSEKILLER(x1).
-TAKESTOME(x1) | INHOUSE(x1).
-KANGAROO(x1) | -SUITABLEPET(x1). 
-MOUSEKILLER(x1) | CARNIVORE(x1).
TAKESTOME(x1) | DETESTED(x1).
-PROWLER(x1) | GAZER(x1). 
KANGAROO(x1).
-AVOIDED(f1).
SHAR_EOF
if test -f 'animals.ver1.in'
then
	echo shar: over-writing existing file "'animals.ver1.in'"
fi
cat << \SHAR_EOF > 'animals.ver1.in'
% problem-set/puzzles/carroll/animals.ver1.in
% created : 07/09/86
% revised : 07/05/88 

% description:
%
% This run solves a puzzle called "The Animals" by Lewis Carroll
% using UR-resolution.
%
%                       The Animals
%
%    (1)  The only animals in this house are cats.
%    (2)  Every animal is suitable for a pet, that loves  to
%         gaze at the moon.
%    (3)  When I detest an animal, I avoid it.
%    (4)  No animals are carnivorous, unless they  prowl  at
%         night.
%    (5)  No cat fails to kill mice.
%    (6)  No animals ever take to me,  except  what  are  in
%         this house.
%    (7)  Kangaroos are not suitable for pets.
%    (8)  None but carnivora kill mice.
%    (9)  I detest animals that do not take to me.
%    (10) Animals that prowl at night always love to gaze at
%         the moon.
%    The problem is to prove that "I  always  avoid  a  kan-
%    garoo".
%                                        - Lewis Carroll
%

% representation:
% 
% declare_predicates(1,[INHOUSE,CAT,GAZER,SUITABLEPET,DETESTED,AVOIDED])
% declare_predicates(1,[CARNIVORE,PROWLER,MOUSEKILLER,TAKESTOME,KANGAROO])
% declare_constant(f1).   
% declare_variable(x1).
% 
% Declarative version,  created by E. Lusk    
% PREDICATES : CAT(x) = x is a cat.
%    INHOUSE(x) = x is an animal in the house.
%    SUITABLEPET= an animal suitable for a pet.
%    PROWLER= animals who prowl at night.
                  
set(UR_res).


list(axioms).

-INHOUSE(x1) | CAT(x1).
-GAZER(x1) | SUITABLEPET(x1).
-DETESTED(x1) | AVOIDED(x1). 
-CARNIVORE(x1) | PROWLER(x1).
-CAT(x1) | MOUSEKILLER(x1).
-TAKESTOME(x1) | INHOUSE(x1).
-KANGAROO(x1) | -SUITABLEPET(x1). 
-MOUSEKILLER(x1) | CARNIVORE(x1).
TAKESTOME(x1) | DETESTED(x1).
-PROWLER(x1) | GAZER(x1). 

end_of_list.


list(sos).

KANGAROO(x1).
-AVOIDED(f1).
 
end_of_list.
SHAR_EOF
if test -f 'animals.ver1.out'
then
	echo shar: over-writing existing file "'animals.ver1.out'"
fi
cat << \SHAR_EOF > 'animals.ver1.out'
problem-set/puzzles/carroll/animals.ver1.out
created : 07/05/88
revised : 07/14/88

OTTER release 0.9, 19 May 1988

set(UR_res).

list(axioms).
1 -INHOUSE(x1) | CAT(x1).
2 -GAZER(x1) | SUITABLEPET(x1).
3 -DETESTED(x1) | AVOIDED(x1).
4 -CARNIVORE(x1) | PROWLER(x1).
5 -CAT(x1) | MOUSEKILLER(x1).
6 -TAKESTOME(x1) | INHOUSE(x1).
7 -KANGAROO(x1) | -SUITABLEPET(x1).
8 -MOUSEKILLER(x1) | CARNIVORE(x1).
9 TAKESTOME(x1) | DETESTED(x1).
10 -PROWLER(x1) | GAZER(x1).
end_of_list.

list(sos).
11 KANGAROO(x1).
12 -AVOIDED(f1).
end_of_list.

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

1 -INHOUSE(x1) | CAT(x1).
2 -GAZER(x1) | SUITABLEPET(x1).
3 -DETESTED(x1) | AVOIDED(x1).
4 -CARNIVORE(x1) | PROWLER(x1).
5 -CAT(x1) | MOUSEKILLER(x1).
6 -TAKESTOME(x1) | INHOUSE(x1).
7 -KANGAROO(x1) | -SUITABLEPET(x1).
8 -MOUSEKILLER(x1) | CARNIVORE(x1).
9 TAKESTOME(x1) | DETESTED(x1).
10 -PROWLER(x1) | GAZER(x1).
11 KANGAROO(x1).
12 -AVOIDED(f1).
13 (11,7) -SUITABLEPET(x).
14 (12,3) -DETESTED(f1).
15 (13,2) -GAZER(x).
16 (14,9) TAKESTOME(f1).
17 (15,10) -PROWLER(x).
18 (16,6) INHOUSE(f1).
19 (17,4) -CARNIVORE(x).
20 (18,1) CAT(f1).
21 (19,8) -MOUSEKILLER(x).
22 (20,5) MOUSEKILLER(f1).
23 (22,21) .

--------------- options ---------------
set(UR_res).
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(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
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).

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, 4).
assign(fpa_terms, 4).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                 12
clauses given                 10
clauses generated             11
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                  11
empty clauses                  1
factors generated              0
clauses back subsumed          5
clauses not processed          2

----------- times (seconds) -----------
run time             0.35
input time           0.12
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.04
  demod time         0.00
  weigh time         0.00
  for_sub time       0.00
  unit_del time      0.00
post_process time    0.03
  back_sub time      0.00
  conflict time      0.01
  factor time        0.00
FPA build time       0.02
IS build time        0.01
print_cl time        0.09
cl integrate time    0.01
window time          0.00
SHAR_EOF
if test -f 'boys.desc'
then
	echo shar: over-writing existing file "'boys.desc'"
fi
cat << \SHAR_EOF > 'boys.desc'
problem-set/puzzles/carroll/boys.desc
created : 07/09/86
revised : 07/12/88
 
Natural Language Description:

                              The School Boys
        
        "All the boys, in a certain  school,  sit  together  in  one
        large  room  every  evening.   They are of no less than five
        nationalities - English, Scotch, Welsh, Irish,  and  German.
        One  of  the  Monitors (who is a great reader of Wilkie Col-
        lins' novels) is very  observant  and  takes  MS.  notes  of
        almost  everything  that  happens,  with the view of being a
        good sensational witness, in case any conspiracy to commit a
        murder  should  be  afoot.   The  following  are some of his
        notes:
        
        (1)  Whenever some of the English boys  are  singing  "Rule,
             Britannia," and some not, some of the Monitors are wide
             awake;
        
        (2)  Whenever some of the Scotch are dancing reels, and some
             of  the  Irish  fighting,  some of the Welsh are eating
             toasted cheese;
        
        (3)  Whenever all the Germans are playing chess, some of the
             Eleven are not oiling their bats;
        
        (4)  Whenever some of the Monitors are asleep, and some not,
             some of the Irish are fighting.
        
        (5)  Whenever some of the Germans  are  playing  chess,  and
             none of the Scotch are dancing reels, some of the Welsh
             are not eating toasted cheese.
        
        (6)  Whenever some of the Scotch are not dancing reels,  and
             some of the Irish are not fighting, some of the Germans
             are playing chess;
        
        (7)  Whenever some of the Monitors are awake,  and  some  of
             the Welsh are eating toasted cheese, none of the Scotch
             are dancing reels;
        
        (8)  Whenever some of the Germans are not playing chess, and
             some  of  the Welsh are not eating toasted cheese, none
             of the Irish are fighting;
        
        (9)  Whenever all of the English are singing "Rule,  Britan-
             nia,"  and  some  of  the Scotch are not dancing reels,
             none of the Germans are playing chess;
        
        (10) Whenever some of the English are singing "Rule, Britan-
             nia,", and some of the Monitors are asleep, some of the
             Irish are not fighting;
        
        (11) Whenever some of the Monitors are awake,  and  some  of
             the  Eleven  are  not  oiling  their  bats, some of the
             Scotch are dancing reels;
        
        (12) Whenever some of the English are singing "Rule, Britan-
             nia," and some of the Scotch are not dancing reels, ...
        
        Here the MS. breaks off suddenly.  The problem  is  to  com-
        plete the sentence, if possible."
                                - Lewis Carroll

Versions:

boys.ver1.in : Declarative representation. The solution is clause
	114 of the output file, -Some_monitors_are_not_awake.

		created by : E. Lusk
		verified for ITP : 07/09/86
		translated for OTTER by : K.R.
		verified for OTTER : 07/12/88
SHAR_EOF
if test -f 'boys.ver1.clauses'
then
	echo shar: over-writing existing file "'boys.ver1.clauses'"
fi
cat << \SHAR_EOF > 'boys.ver1.clauses'
% problem-set/puzzles/carroll/boys.ver1.clauses
% created : 07/12/88
% revised : 07/12/88
 
% description:
%
% This run solves a puzzle called "The School Boys" using binary and UR-
% resolution.
% 
%                               The School Boys
%         
%         "All the boys, in a certain  school,  sit  together  in  one
%         large  room  every  evening.   They are of no less than five
%         nationalities - English, Scotch, Welsh, Irish,  and  German.
%         One  of  the  Monitors (who is a great reader of Wilkie Col-
%         lins' novels) is very  observant  and  takes  MS.  notes  of
%         almost  everything  that  happens,  with the view of being a
%         good sensational witness, in case any conspiracy to commit a
%         murder  should  be  afoot.   The  following  are some of his
%         notes:
%         
%         (1)  Whenever some of the English boys  are  singing  "Rule,
%              Britannia," and some not, some of the Monitors are wide
%              awake;
%         
%         (2)  Whenever some of the Scotch are dancing reels, and some
%              of  the  Irish  fighting,  some of the Welsh are eating
%              toasted cheese;
%         
%         (3)  Whenever all the Germans are playing chess, some of the
%              Eleven are not oiling their bats;
%         
%         (4)  Whenever some of the Monitors are asleep, and some not,
%              some of the Irish are fighting.
%         
%         (5)  Whenever some of the Germans  are  playing  chess,  and
%              none of the Scotch are dancing reels, some of the Welsh
%              are not eating toasted cheese.
%         
%         (6)  Whenever some of the Scotch are not dancing reels,  and
%              some of the Irish are not fighting, some of the Germans
%              are playing chess;
%         
%         (7)  Whenever some of the Monitors are awake,  and  some  of
%              the Welsh are eating toasted cheese, none of the Scotch
%              are dancing reels;
%         
%         (8)  Whenever some of the Germans are not playing chess, and
%              some  of  the Welsh are not eating toasted cheese, none
%              of the Irish are fighting;
%         
%         (9)  Whenever all of the English are singing "Rule,  Britan-
%              nia,"  and  some  of  the Scotch are not dancing reels,
%              none of the Germans are playing chess;
%         
%         (10) Whenever some of the English are singing "Rule, Britan-
%              nia,", and some of the Monitors are asleep, some of the
%              Irish are not fighting;
%         
%         (11) Whenever some of the Monitors are awake,  and  some  of
%              the  Eleven  are  not  oiling  their  bats, some of the
%              Scotch are dancing reels;
%         
%         (12) Whenever some of the English are singing "Rule, Britan-
%              nia," and some of the Scotch are not dancing reels, ...
%         
%         Here the MS. breaks off suddenly.  The problem  is  to  com-
%         plete the sentence, if possible."
%                                                     - Lewis Carroll

% representation:
%
% Declarative version. Originally created by E. Lusk, and used hyper-
% resolution and weights. The solution is clause 114 of the output
% file, "-Some_monitors_are_not_awake"

-Some_English_sing | -Some_English_sing_not | 
    Some_monitors_are_awake.
-Some_Scotch_dance | -Some_Irish_fight |
    Some_Welsh_eat.
-Some_Germans_play | Some_Germans_play_not |
    Some_of_the_eleven_are_not_oiling.
-Some_monitors_are_awake | -Some_monitors_are_not_awake |
    Some_Irish_fight.
-Some_Germans_play | Some_Scotch_dance |
    Some_Welsh_eat_not.
-Some_Scotch_dance_not | -Some_Irish_fight_not |
    Some_Germans_play.
-Some_monitors_are_awake | -Some_Welsh_eat |
   -Some_Scotch_dance.
-Some_Germans_play_not | -Some_Welsh_eat_not |
    -Some_Irish_fight.
-Some_English_sing | Some_English_sing_not | -
   Some_Scotch_dance_not |
    -Some_Germans_play.
-Some_English_sing | -Some_monitors_are_not_awake |
    Some_Irish_fight_not.
-Some_monitors_are_awake | -Some_of_the_eleven_are_not_oiling |
    Some_Scotch_dance.
Some_English_sing_not | Some_English_sing.
Some_monitors_are_not_awake | Some_monitors_are_awake.
Some_Scotch_dance | Some_Scotch_dance_not.
Some_Irish_fight | Some_Irish_fight_not.
Some_Welsh_eat | Some_Welsh_eat_not.
Some_Germans_play | Some_Germans_play_not.
Some_English_sing.
Some_Scotch_dance_not.
SHAR_EOF
if test -f 'boys.ver1.in'
then
	echo shar: over-writing existing file "'boys.ver1.in'"
fi
cat << \SHAR_EOF > 'boys.ver1.in'
% problem-set/puzzles/carroll/boys.ver1.in
% created : 07/09/86
% revised : 07/12/88
 
% description:
%
% This run solves a puzzle called "The School Boys" using binary and UR-
% resolution.
% 
%                               The School Boys
%         
%         "All the boys, in a certain  school,  sit  together  in  one
%         large  room  every  evening.   They are of no less than five
%         nationalities - English, Scotch, Welsh, Irish,  and  German.
%         One  of  the  Monitors (who is a great reader of Wilkie Col-
%         lins' novels) is very  observant  and  takes  MS.  notes  of
%         almost  everything  that  happens,  with the view of being a
%         good sensational witness, in case any conspiracy to commit a
%         murder  should  be  afoot.   The  following  are some of his
%         notes:
%         
%         (1)  Whenever some of the English boys  are  singing  "Rule,
%              Britannia," and some not, some of the Monitors are wide
%              awake;
%         
%         (2)  Whenever some of the Scotch are dancing reels, and some
%              of  the  Irish  fighting,  some of the Welsh are eating
%              toasted cheese;
%         
%         (3)  Whenever all the Germans are playing chess, some of the
%              Eleven are not oiling their bats;
%         
%         (4)  Whenever some of the Monitors are asleep, and some not,
%              some of the Irish are fighting.
%         
%         (5)  Whenever some of the Germans  are  playing  chess,  and
%              none of the Scotch are dancing reels, some of the Welsh
%              are not eating toasted cheese.
%         
%         (6)  Whenever some of the Scotch are not dancing reels,  and
%              some of the Irish are not fighting, some of the Germans
%              are playing chess;
%         
%         (7)  Whenever some of the Monitors are awake,  and  some  of
%              the Welsh are eating toasted cheese, none of the Scotch
%              are dancing reels;
%         
%         (8)  Whenever some of the Germans are not playing chess, and
%              some  of  the Welsh are not eating toasted cheese, none
%              of the Irish are fighting;
%         
%         (9)  Whenever all of the English are singing "Rule,  Britan-
%              nia,"  and  some  of  the Scotch are not dancing reels,
%              none of the Germans are playing chess;
%         
%         (10) Whenever some of the English are singing "Rule, Britan-
%              nia,", and some of the Monitors are asleep, some of the
%              Irish are not fighting;
%         
%         (11) Whenever some of the Monitors are awake,  and  some  of
%              the  Eleven  are  not  oiling  their  bats, some of the
%              Scotch are dancing reels;
%         
%         (12) Whenever some of the English are singing "Rule, Britan-
%              nia," and some of the Scotch are not dancing reels, ...
%         
%         Here the MS. breaks off suddenly.  The problem  is  to  com-
%         plete the sentence, if possible."
%                                                     - Lewis Carroll

% representation:
% 
% Declarative version. Originally created by E. Lusk, and used hyper-
% resolution and weights. The solution is clause 114 of the output
% file, "-Some_monitors_are_not_awake"

set(binary_res).
set(UR_res).


list(axioms).

-Some_English_sing | -Some_English_sing_not | 
    Some_monitors_are_awake.
-Some_Scotch_dance | -Some_Irish_fight |
    Some_Welsh_eat.
-Some_Germans_play | Some_Germans_play_not |
    Some_of_the_eleven_are_not_oiling.
-Some_monitors_are_awake | -Some_monitors_are_not_awake |
    Some_Irish_fight.
-Some_Germans_play | Some_Scotch_dance |
    Some_Welsh_eat_not.
-Some_Scotch_dance_not | -Some_Irish_fight_not |
    Some_Germans_play.
-Some_monitors_are_awake | -Some_Welsh_eat |
   -Some_Scotch_dance.
-Some_Germans_play_not | -Some_Welsh_eat_not |
    -Some_Irish_fight.
-Some_English_sing | Some_English_sing_not | -
   Some_Scotch_dance_not |
    -Some_Germans_play.
-Some_English_sing | -Some_monitors_are_not_awake |
    Some_Irish_fight_not.
-Some_monitors_are_awake | -Some_of_the_eleven_are_not_oiling |
    Some_Scotch_dance.

end_of_list.


list(sos).

Some_English_sing_not | Some_English_sing.
Some_monitors_are_not_awake | Some_monitors_are_awake.
Some_Scotch_dance | Some_Scotch_dance_not.
Some_Irish_fight | Some_Irish_fight_not.
Some_Welsh_eat | Some_Welsh_eat_not.
Some_Germans_play | Some_Germans_play_not.
Some_English_sing.
Some_Scotch_dance_not.

end_of_list.
SHAR_EOF
if test -f 'boys.ver1.out'
then
	echo shar: over-writing existing file "'boys.ver1.out'"
fi
cat << \SHAR_EOF > 'boys.ver1.out'
problem-set/puzzles/carroll/boys.ver1.out
created : 07/09/88
revised : 07/14/88

OTTER version 0.9, 19 May 1988.

set(binary_res).
set(UR_res).

list(axioms).
1 -Some_English_sing | -Some_English_sing_not | Some_monitors_are_awake.
2 -Some_Scotch_dance | -Some_Irish_fight | Some_Welsh_eat.
3 -Some_Germans_play | Some_Germans_play_not | Some_of_the_eleven_are_not_oiling.
4 -Some_monitors_are_awake | -Some_monitors_are_not_awake | Some_Irish_fight.
5 -Some_Germans_play | Some_Scotch_dance | Some_Welsh_eat_not.
6 -Some_Scotch_dance_not | -Some_Irish_fight_not | Some_Germans_play.
7 -Some_monitors_are_awake | -Some_Welsh_eat | -Some_Scotch_dance.
8 -Some_Germans_play_not | -Some_Welsh_eat_not | -Some_Irish_fight.
9 -Some_English_sing | Some_English_sing_not | -Some_Scotch_dance_not | -Some_Germans_play.
10 -Some_English_sing | -Some_monitors_are_not_awake | Some_Irish_fight_not.
11 -Some_monitors_are_awake | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
end_of_list.

list(sos).
12 Some_English_sing_not | Some_English_sing.
13 Some_monitors_are_not_awake | Some_monitors_are_awake.
14 Some_Scotch_dance | Some_Scotch_dance_not.
15 Some_Irish_fight | Some_Irish_fight_not.
16 Some_Welsh_eat | Some_Welsh_eat_not.
17 Some_Germans_play | Some_Germans_play_not.
18 Some_English_sing.
19 Some_Scotch_dance_not.
end_of_list.

new given clause: 18 Some_English_sing.
** KEPT: 20 (18,10) -Some_monitors_are_not_awake | Some_Irish_fight_not.
** KEPT: 21 (18,9) Some_English_sing_not | -Some_Scotch_dance_not | -Some_Germans_play.
** KEPT: 22 (18,1) -Some_English_sing_not | Some_monitors_are_awake.
20 back subsumes: 10 -Some_English_sing | -Some_monitors_are_not_awake | Some_Irish_fight_not.
21 back subsumes: 9 -Some_English_sing | Some_English_sing_not | -Some_Scotch_dance_not | -Some_Germans_play.
22 back subsumes: 1 -Some_English_sing | -Some_English_sing_not | Some_monitors_are_awake.

new given clause: 19 Some_Scotch_dance_not.
** KEPT: 23 (19,6) -Some_Irish_fight_not | Some_Germans_play.
23 back subsumes: 6 -Some_Scotch_dance_not | -Some_Irish_fight_not | Some_Germans_play.

new given clause: 12 Some_English_sing_not | Some_English_sing.

new given clause: 13 Some_monitors_are_not_awake | Some_monitors_are_awake.
** KEPT: 24 (13,11) Some_monitors_are_not_awake | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 25 (13,7) Some_monitors_are_not_awake | -Some_Welsh_eat | -Some_Scotch_dance.

new given clause: 14 Some_Scotch_dance | Some_Scotch_dance_not.

new given clause: 15 Some_Irish_fight | Some_Irish_fight_not.
** KEPT: 26 (15,8) Some_Irish_fight_not | -Some_Germans_play_not | -Some_Welsh_eat_not.
** KEPT: 27 (15,2) Some_Irish_fight_not | -Some_Scotch_dance | Some_Welsh_eat.

new given clause: 16 Some_Welsh_eat | Some_Welsh_eat_not.
** KEPT: 28 (16,7) Some_Welsh_eat_not | -Some_monitors_are_awake | -Some_Scotch_dance.
** KEPT: 29 (16,8) Some_Welsh_eat | -Some_Germans_play_not | -Some_Irish_fight.

new given clause: 17 Some_Germans_play | Some_Germans_play_not.
** KEPT: 30 (17,5) Some_Germans_play_not | Some_Scotch_dance | Some_Welsh_eat_not.
** KEPT: 31 (17,3) Some_Germans_play_not | Some_of_the_eleven_are_not_oiling.
** KEPT: 32 (17,8) Some_Germans_play | -Some_Welsh_eat_not | -Some_Irish_fight.
31 back subsumes: 3 -Some_Germans_play | Some_Germans_play_not | Some_of_the_eleven_are_not_oiling.

new given clause: 20 (18,10) -Some_monitors_are_not_awake | Some_Irish_fight_not.
** KEPT: 33 (20,13) Some_Irish_fight_not | Some_monitors_are_awake.

new given clause: 22 (18,1) -Some_English_sing_not | Some_monitors_are_awake.
** KEPT: 34 (22,11) -Some_English_sing_not | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 35 (22,7) -Some_English_sing_not | -Some_Welsh_eat | -Some_Scotch_dance.
** KEPT: 36 (22,4) -Some_English_sing_not | -Some_monitors_are_not_awake | Some_Irish_fight.

new given clause: 23 (19,6) -Some_Irish_fight_not | Some_Germans_play.
** KEPT: 37 (23,20) Some_Germans_play | -Some_monitors_are_not_awake.
** KEPT: 38 (23,15) Some_Germans_play | Some_Irish_fight.
** KEPT: 39 (23,5) -Some_Irish_fight_not | Some_Scotch_dance | Some_Welsh_eat_not.

new given clause: 31 (17,3) Some_Germans_play_not | Some_of_the_eleven_are_not_oiling.
** KEPT: 40 (31,8) Some_of_the_eleven_are_not_oiling | -Some_Welsh_eat_not | -Some_Irish_fight.
** KEPT: 41 (31,11) Some_Germans_play_not | -Some_monitors_are_awake | Some_Scotch_dance.

new given clause: 33 (20,13) Some_Irish_fight_not | Some_monitors_are_awake.
** KEPT: 42 (33,23) Some_monitors_are_awake | Some_Germans_play.
** KEPT: 43 (33,11) Some_Irish_fight_not | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 44 (33,7) Some_Irish_fight_not | -Some_Welsh_eat | -Some_Scotch_dance.

new given clause: 37 (23,20) Some_Germans_play | -Some_monitors_are_not_awake.
** KEPT: 45 (37,5) -Some_monitors_are_not_awake | Some_Scotch_dance | Some_Welsh_eat_not.

new given clause: 38 (23,15) Some_Germans_play | Some_Irish_fight.
** KEPT: 46 (38,5) Some_Irish_fight | Some_Scotch_dance | Some_Welsh_eat_not.
** KEPT: 47 (38,8) Some_Germans_play | -Some_Germans_play_not | -Some_Welsh_eat_not.
** KEPT: 48 (38,2) Some_Germans_play | -Some_Scotch_dance | Some_Welsh_eat.

new given clause: 42 (33,23) Some_monitors_are_awake | Some_Germans_play.
** KEPT: 49 (42,11) Some_Germans_play | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 50 (42,7) Some_Germans_play | -Some_Welsh_eat | -Some_Scotch_dance.
** KEPT: 51 (42,5) Some_monitors_are_awake | Some_Scotch_dance | Some_Welsh_eat_not.

new given clause: 21 (18,9) Some_English_sing_not | -Some_Scotch_dance_not | -Some_Germans_play.
** KEPT: 52 (21,22) -Some_Scotch_dance_not | -Some_Germans_play | Some_monitors_are_awake.
** KEPT: 53 (21,19) Some_English_sing_not | -Some_Germans_play.
** KEPT: 54 (21,42) Some_English_sing_not | -Some_Scotch_dance_not | Some_monitors_are_awake.
** KEPT: 55 (21,38) Some_English_sing_not | -Some_Scotch_dance_not | Some_Irish_fight.
** KEPT: 56 (21,37) Some_English_sing_not | -Some_Scotch_dance_not | -Some_monitors_are_not_awake.
** KEPT: 57 (21,23) Some_English_sing_not | -Some_Scotch_dance_not | -Some_Irish_fight_not.
** KEPT: 58 (21,17) Some_English_sing_not | -Some_Scotch_dance_not | Some_Germans_play_not.
53 back subsumes: 21 (18,9) Some_English_sing_not | -Some_Scotch_dance_not | -Some_Germans_play.

new given clause: 53 (21,19) Some_English_sing_not | -Some_Germans_play.
** KEPT: 59 (53,22) -Some_Germans_play | Some_monitors_are_awake.
** KEPT: 60 (53,42) Some_English_sing_not | Some_monitors_are_awake.
** KEPT: 61 (53,38) Some_English_sing_not | Some_Irish_fight.
** KEPT: 62 (53,37) Some_English_sing_not | -Some_monitors_are_not_awake.
** KEPT: 63 (53,23) Some_English_sing_not | -Some_Irish_fight_not.
** KEPT: 64 (53,17) Some_English_sing_not | Some_Germans_play_not.
59 back subsumes: 52 (21,22) -Some_Scotch_dance_not | -Some_Germans_play | Some_monitors_are_awake.
60 back subsumes: 54 (21,42) Some_English_sing_not | -Some_Scotch_dance_not | Some_monitors_are_awake.
61 back subsumes: 55 (21,38) Some_English_sing_not | -Some_Scotch_dance_not | Some_Irish_fight.
62 back subsumes: 56 (21,37) Some_English_sing_not | -Some_Scotch_dance_not | -Some_monitors_are_not_awake.
63 back subsumes: 57 (21,23) Some_English_sing_not | -Some_Scotch_dance_not | -Some_Irish_fight_not.
64 back subsumes: 58 (21,17) Some_English_sing_not | -Some_Scotch_dance_not | Some_Germans_play_not.

new given clause: 59 (53,22) -Some_Germans_play | Some_monitors_are_awake.
** KEPT: 65 (59,42) Some_monitors_are_awake.
** KEPT: 66 (59,11) -Some_Germans_play | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 67 (59,7) -Some_Germans_play | -Some_Welsh_eat | -Some_Scotch_dance.
** KEPT: 68 (59,4) -Some_Germans_play | -Some_monitors_are_not_awake | Some_Irish_fight.
65 back subsumes: 60 (53,42) Some_English_sing_not | Some_monitors_are_awake.
65 back subsumes: 59 (53,22) -Some_Germans_play | Some_monitors_are_awake.
65 back subsumes: 51 (42,5) Some_monitors_are_awake | Some_Scotch_dance | Some_Welsh_eat_not.
65 back subsumes: 42 (33,23) Some_monitors_are_awake | Some_Germans_play.
65 back subsumes: 33 (20,13) Some_Irish_fight_not | Some_monitors_are_awake.
65 back subsumes: 22 (18,1) -Some_English_sing_not | Some_monitors_are_awake.
65 back subsumes: 13 Some_monitors_are_not_awake | Some_monitors_are_awake.

new given clause: 65 (59,42) Some_monitors_are_awake.
** KEPT: 69 (65,11) -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 70 (65,7) -Some_Welsh_eat | -Some_Scotch_dance.
** KEPT: 71 (65,4) -Some_monitors_are_not_awake | Some_Irish_fight.
69 back subsumes: 66 (59,11) -Some_Germans_play | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
69 back subsumes: 49 (42,11) Some_Germans_play | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
69 back subsumes: 43 (33,11) Some_Irish_fight_not | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
69 back subsumes: 34 (22,11) -Some_English_sing_not | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
69 back subsumes: 24 (13,11) Some_monitors_are_not_awake | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
69 back subsumes: 11 -Some_monitors_are_awake | -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
70 back subsumes: 67 (59,7) -Some_Germans_play | -Some_Welsh_eat | -Some_Scotch_dance.
70 back subsumes: 50 (42,7) Some_Germans_play | -Some_Welsh_eat | -Some_Scotch_dance.
70 back subsumes: 44 (33,7) Some_Irish_fight_not | -Some_Welsh_eat | -Some_Scotch_dance.
70 back subsumes: 35 (22,7) -Some_English_sing_not | -Some_Welsh_eat | -Some_Scotch_dance.
70 back subsumes: 25 (13,7) Some_monitors_are_not_awake | -Some_Welsh_eat | -Some_Scotch_dance.
70 back subsumes: 7 -Some_monitors_are_awake | -Some_Welsh_eat | -Some_Scotch_dance.
71 back subsumes: 68 (59,4) -Some_Germans_play | -Some_monitors_are_not_awake | Some_Irish_fight.
71 back subsumes: 36 (22,4) -Some_English_sing_not | -Some_monitors_are_not_awake | Some_Irish_fight.
71 back subsumes: 4 -Some_monitors_are_awake | -Some_monitors_are_not_awake | Some_Irish_fight.

new given clause: 61 (53,38) Some_English_sing_not | Some_Irish_fight.
** KEPT: 72 (61,8) Some_English_sing_not | -Some_Germans_play_not | -Some_Welsh_eat_not.
** KEPT: 73 (61,2) Some_English_sing_not | -Some_Scotch_dance | Some_Welsh_eat.

new given clause: 62 (53,37) Some_English_sing_not | -Some_monitors_are_not_awake.

new given clause: 63 (53,23) Some_English_sing_not | -Some_Irish_fight_not.

new given clause: 64 (53,17) Some_English_sing_not | Some_Germans_play_not.
** KEPT: 74 (64,8) Some_English_sing_not | -Some_Welsh_eat_not | -Some_Irish_fight.

new given clause: 69 (65,11) -Some_of_the_eleven_are_not_oiling | Some_Scotch_dance.
** KEPT: 75 (69,31) Some_Scotch_dance | Some_Germans_play_not.
** KEPT: 76 (69,2) -Some_of_the_eleven_are_not_oiling | -Some_Irish_fight | Some_Welsh_eat.
75 back subsumes: 41 (31,11) Some_Germans_play_not | -Some_monitors_are_awake | Some_Scotch_dance.
75 back subsumes: 30 (17,5) Some_Germans_play_not | Some_Scotch_dance | Some_Welsh_eat_not.

new given clause: 70 (65,7) -Some_Welsh_eat | -Some_Scotch_dance.
** KEPT: 77 (70,16) -Some_Scotch_dance | Some_Welsh_eat_not.
** KEPT: 78 (70,2) -Some_Scotch_dance | -Some_Irish_fight.
** KEPT: 79 (70,69) -Some_Welsh_eat | -Some_of_the_eleven_are_not_oiling.
** KEPT: 80 (70,5) -Some_Welsh_eat | -Some_Germans_play | Some_Welsh_eat_not.
77 back subsumes: 28 (16,7) Some_Welsh_eat_not | -Some_monitors_are_awake | -Some_Scotch_dance.
78 back subsumes: 2 -Some_Scotch_dance | -Some_Irish_fight | Some_Welsh_eat.

new given clause: 71 (65,4) -Some_monitors_are_not_awake | Some_Irish_fight.
** KEPT: 81 (71,8) -Some_monitors_are_not_awake | -Some_Germans_play_not | -Some_Welsh_eat_not.

new given clause: 75 (69,31) Some_Scotch_dance | Some_Germans_play_not.
** KEPT: 82 (75,70) Some_Germans_play_not | -Some_Welsh_eat.
** KEPT: 83 (75,8) Some_Scotch_dance | -Some_Welsh_eat_not | -Some_Irish_fight.

new given clause: 77 (70,16) -Some_Scotch_dance | Some_Welsh_eat_not.
** KEPT: 84 (77,75) Some_Welsh_eat_not | Some_Germans_play_not.
** KEPT: 85 (77,69) Some_Welsh_eat_not | -Some_of_the_eleven_are_not_oiling.
** KEPT: 86 (77,5) Some_Welsh_eat_not | -Some_Germans_play.
86 back subsumes: 80 (70,5) -Some_Welsh_eat | -Some_Germans_play | Some_Welsh_eat_not.
86 back subsumes: 5 -Some_Germans_play | Some_Scotch_dance | Some_Welsh_eat_not.

new given clause: 78 (70,2) -Some_Scotch_dance | -Some_Irish_fight.
** KEPT: 87 (78,75) -Some_Irish_fight | Some_Germans_play_not.
** KEPT: 88 (78,69) -Some_Irish_fight | -Some_of_the_eleven_are_not_oiling.
** KEPT: 89 (78,71) -Some_Scotch_dance | -Some_monitors_are_not_awake.
** KEPT: 90 (78,61) -Some_Scotch_dance | Some_English_sing_not.
** KEPT: 91 (78,38) -Some_Scotch_dance | Some_Germans_play.
** KEPT: 92 (78,15) -Some_Scotch_dance | Some_Irish_fight_not.
88 back subsumes: 76 (69,2) -Some_of_the_eleven_are_not_oiling | -Some_Irish_fight | Some_Welsh_eat.
90 back subsumes: 73 (61,2) Some_English_sing_not | -Some_Scotch_dance | Some_Welsh_eat.
91 back subsumes: 48 (38,2) Some_Germans_play | -Some_Scotch_dance | Some_Welsh_eat.
92 back subsumes: 27 (15,2) Some_Irish_fight_not | -Some_Scotch_dance | Some_Welsh_eat.

new given clause: 79 (70,69) -Some_Welsh_eat | -Some_of_the_eleven_are_not_oiling.

new given clause: 82 (75,70) Some_Germans_play_not | -Some_Welsh_eat.
** KEPT: 93 (82,8) -Some_Welsh_eat | -Some_Welsh_eat_not | -Some_Irish_fight.

new given clause: 84 (77,75) Some_Welsh_eat_not | Some_Germans_play_not.

new given clause: 85 (77,69) Some_Welsh_eat_not | -Some_of_the_eleven_are_not_oiling.

new given clause: 86 (77,5) Some_Welsh_eat_not | -Some_Germans_play.
** KEPT: 94 (86,8) -Some_Germans_play | -Some_Germans_play_not | -Some_Irish_fight.
** KEPT: 95 (86,38) Some_Welsh_eat_not | Some_Irish_fight.
** KEPT: 96 (86,37) Some_Welsh_eat_not | -Some_monitors_are_not_awake.
** KEPT: 97 (86,23) Some_Welsh_eat_not | -Some_Irish_fight_not.
95 back subsumes: 46 (38,5) Some_Irish_fight | Some_Scotch_dance | Some_Welsh_eat_not.
96 back subsumes: 45 (37,5) -Some_monitors_are_not_awake | Some_Scotch_dance | Some_Welsh_eat_not.
97 back subsumes: 39 (23,5) -Some_Irish_fight_not | Some_Scotch_dance | Some_Welsh_eat_not.

new given clause: 87 (78,75) -Some_Irish_fight | Some_Germans_play_not.
** KEPT: 98 (87,71) Some_Germans_play_not | -Some_monitors_are_not_awake.
** KEPT: 99 (87,15) Some_Germans_play_not | Some_Irish_fight_not.
** KEPT: 100 (87,8) -Some_Irish_fight | -Some_Welsh_eat_not.
100 back subsumes: 93 (82,8) -Some_Welsh_eat | -Some_Welsh_eat_not | -Some_Irish_fight.
100 back subsumes: 83 (75,8) Some_Scotch_dance | -Some_Welsh_eat_not | -Some_Irish_fight.
100 back subsumes: 74 (64,8) Some_English_sing_not | -Some_Welsh_eat_not | -Some_Irish_fight.
100 back subsumes: 40 (31,8) Some_of_the_eleven_are_not_oiling | -Some_Welsh_eat_not | -Some_Irish_fight.
100 back subsumes: 32 (17,8) Some_Germans_play | -Some_Welsh_eat_not | -Some_Irish_fight.
100 back subsumes: 8 -Some_Germans_play_not | -Some_Welsh_eat_not | -Some_Irish_fight.

new given clause: 88 (78,69) -Some_Irish_fight | -Some_of_the_eleven_are_not_oiling.
** KEPT: 101 (88,71) -Some_of_the_eleven_are_not_oiling | -Some_monitors_are_not_awake.
** KEPT: 102 (88,61) -Some_of_the_eleven_are_not_oiling | Some_English_sing_not.
** KEPT: 103 (88,38) -Some_of_the_eleven_are_not_oiling | Some_Germans_play.
** KEPT: 104 (88,15) -Some_of_the_eleven_are_not_oiling | Some_Irish_fight_not.

new given clause: 89 (78,71) -Some_Scotch_dance | -Some_monitors_are_not_awake.

new given clause: 90 (78,61) -Some_Scotch_dance | Some_English_sing_not.

new given clause: 91 (78,38) -Some_Scotch_dance | Some_Germans_play.

new given clause: 92 (78,15) -Some_Scotch_dance | Some_Irish_fight_not.

new given clause: 95 (86,38) Some_Welsh_eat_not | Some_Irish_fight.

new given clause: 96 (86,37) Some_Welsh_eat_not | -Some_monitors_are_not_awake.

new given clause: 97 (86,23) Some_Welsh_eat_not | -Some_Irish_fight_not.

new given clause: 98 (87,71) Some_Germans_play_not | -Some_monitors_are_not_awake.

new given clause: 99 (87,15) Some_Germans_play_not | Some_Irish_fight_not.

new given clause: 100 (87,8) -Some_Irish_fight | -Some_Welsh_eat_not.
** KEPT: 105 (100,71) -Some_Welsh_eat_not | -Some_monitors_are_not_awake.
** KEPT: 106 (100,61) -Some_Welsh_eat_not | Some_English_sing_not.
** KEPT: 107 (100,38) -Some_Welsh_eat_not | Some_Germans_play.
** KEPT: 108 (100,15) -Some_Welsh_eat_not | Some_Irish_fight_not.
** KEPT: 109 (100,97) -Some_Irish_fight | -Some_Irish_fight_not.
** KEPT: 110 (100,96) -Some_Irish_fight | -Some_monitors_are_not_awake.
** KEPT: 111 (100,86) -Some_Irish_fight | -Some_Germans_play.
** KEPT: 112 (100,16) -Some_Irish_fight | Some_Welsh_eat.
105 back subsumes: 81 (71,8) -Some_monitors_are_not_awake | -Some_Germans_play_not | -Some_Welsh_eat_not.
106 back subsumes: 72 (61,8) Some_English_sing_not | -Some_Germans_play_not | -Some_Welsh_eat_not.
107 back subsumes: 47 (38,8) Some_Germans_play | -Some_Germans_play_not | -Some_Welsh_eat_not.
108 back subsumes: 26 (15,8) Some_Irish_fight_not | -Some_Germans_play_not | -Some_Welsh_eat_not.
111 back subsumes: 94 (86,8) -Some_Germans_play | -Some_Germans_play_not | -Some_Irish_fight.
112 back subsumes: 29 (16,8) Some_Welsh_eat | -Some_Germans_play_not | -Some_Irish_fight.

new given clause: 101 (88,71) -Some_of_the_eleven_are_not_oiling | -Some_monitors_are_not_awake.

new given clause: 102 (88,61) -Some_of_the_eleven_are_not_oiling | Some_English_sing_not.

new given clause: 103 (88,38) -Some_of_the_eleven_are_not_oiling | Some_Germans_play.

new given clause: 104 (88,15) -Some_of_the_eleven_are_not_oiling | Some_Irish_fight_not.

new given clause: 105 (100,71) -Some_Welsh_eat_not | -Some_monitors_are_not_awake.
** KEPT: 113 (105,97) -Some_monitors_are_not_awake | -Some_Irish_fight_not.
** KEPT: 114 (105,96) -Some_monitors_are_not_awake.
114 back subsumes: 113 (105,97) -Some_monitors_are_not_awake | -Some_Irish_fight_not.
114 back subsumes: 110 (100,96) -Some_Irish_fight | -Some_monitors_are_not_awake.
114 back subsumes: 105 (100,71) -Some_Welsh_eat_not | -Some_monitors_are_not_awake.
114 back subsumes: 101 (88,71) -Some_of_the_eleven_are_not_oiling | -Some_monitors_are_not_awake.
114 back subsumes: 98 (87,71) Some_Germans_play_not | -Some_monitors_are_not_awake.
114 back subsumes: 96 (86,37) Some_Welsh_eat_not | -Some_monitors_are_not_awake.
114 back subsumes: 89 (78,71) -Some_Scotch_dance | -Some_monitors_are_not_awake.
114 back subsumes: 71 (65,4) -Some_monitors_are_not_awake | Some_Irish_fight.
114 back subsumes: 62 (53,37) Some_English_sing_not | -Some_monitors_are_not_awake.
114 back subsumes: 37 (23,20) Some_Germans_play | -Some_monitors_are_not_awake.
114 back subsumes: 20 (18,10) -Some_monitors_are_not_awake | Some_Irish_fight_not.

new given clause: 114 (105,96) -Some_monitors_are_not_awake.

new given clause: 106 (100,61) -Some_Welsh_eat_not | Some_English_sing_not.
** KEPT: 115 (106,16) Some_English_sing_not | Some_Welsh_eat.

new given clause: 107 (100,38) -Some_Welsh_eat_not | Some_Germans_play.
** KEPT: 116 (107,16) Some_Germans_play | Some_Welsh_eat.

new given clause: 108 (100,15) -Some_Welsh_eat_not | Some_Irish_fight_not.
** KEPT: 117 (108,86) Some_Irish_fight_not | -Some_Germans_play.
** KEPT: 118 (108,16) Some_Irish_fight_not | Some_Welsh_eat.

new given clause: 109 (100,97) -Some_Irish_fight | -Some_Irish_fight_not.

new given clause: 111 (100,86) -Some_Irish_fight | -Some_Germans_play.

new given clause: 112 (100,16) -Some_Irish_fight | Some_Welsh_eat.

new given clause: 115 (106,16) Some_English_sing_not | Some_Welsh_eat.

new given clause: 116 (107,16) Some_Germans_play | Some_Welsh_eat.

new given clause: 117 (108,86) Some_Irish_fight_not | -Some_Germans_play.

new given clause: 118 (108,16) Some_Irish_fight_not | Some_Welsh_eat.

------------ END OF SEARCH ------------

sos empty.

--------------- options ---------------
set(binary_res).
set(UR_res).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(hyper_res).
clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
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).

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, 4).
assign(fpa_terms, 4).
assign(demod_limit, 100).
assign(max_proofs, 1).
assign(neg_weight, 0).

-------------- statistics -------------
clauses input                 19
clauses given                 63
clauses generated            249
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted           16
clauses forward subsumed     134
(clauses subsumed by sos)     28
unit deletions                 0
clauses kept                  99
empty clauses                  0
factors generated              0
clauses back subsumed         70
clauses not processed          0

----------- times (seconds) -----------
run time             1.04
input time           0.12
binary_res time      0.14
hyper_res time       0.00
UR_res time          0.08
para_into time       0.00
para_from time       0.00
pre_process time     0.32
  demod time         0.00
  weigh time         0.00
  for_sub time       0.14
  unit_del time      0.00
post_process time    0.28
  back_sub time      0.12
  conflict time      0.00
  factor time        0.00
FPA build time       0.02
IS build time        0.04
print_cl time        0.12
cl integrate time    0.00
window time          0.00
SHAR_EOF
if test -f 'ggson.desc'
then
	echo shar: over-writing existing file "'ggson.desc'"
fi
cat << \SHAR_EOF > 'ggson.desc'
problem-set/puzzles/carroll/ggson.desc
created : 07/14/86
revised : 07/15/88

Natural Language Description:

          	       The Great-grandson Problem

   (1) A man can always master his father.
   (2) An inferior of a man's uncle owes that man money.
   (3) The father of an enemy of a friend of a man owes that man
       nothing.
   (4) A man is always persecuted by his son's creditors.
   (5) An inferior of the master of a man's son is senior to that man.
   (6) A grandson of a man's junior is not his nephew.
   (7) A servant of an inferior of a friend of a man's enemy is never
	   persecuted by that man.
   (8) A friend of a superior of the master of a man's victim is
	   that man's enemy.
   (9) An enemy of a persecutor of a servant of a man's father is that 
	   man's friend.

 	The Problem is to deduce some facts about the great-grandsons.
                   - Lewis Carroll, from "Symbolic Logic" p362.

Versions:

ggson.ver1.in : uses hyper-resolution, UR-resolution, and binary
	resolution. Generates no useful clauses about great-grandsons.

		created by :
		verified for ITP : no proof
		translated for OTTER by : K.R.
		verified for OTTER : no proof
SHAR_EOF
if test -f 'ggson.ver1.clauses'
then
	echo shar: over-writing existing file "'ggson.ver1.clauses'"
fi
cat << \SHAR_EOF > 'ggson.ver1.clauses'
% problem-set/puzzles/carroll/ggson.ver1.clauses
% created : 07/15/88
% revised : 07/15/88

% description:
%
% This run attempts to solve "The Great-grandson Problem" using
% hyper-resolution, binary resolution, and UR-resolution.
% NO PROOF
%
%      THE GREAT-GRANDSON PROBLEM
%                  --- Lewis Carroll from "Symbolic Logic" p362.
%
%  1. A man can always master his father.
%  2. An inferior of a man's uncle owes that man money.
%  3. The father of an enemy of a friend of a man owes that man nothing.
%  4. A man is always persecuted by his son's creditors.
%  5. An inferior of the master of a man's son is senior to that man.
%  6. A grandson of a man's junior is not his nephew.
%  7. A servant of an inferior of a friend of a man's enemy is never
%     persecuted by that man.
%  8. A friend of a superior of the master of a man's victim is that
%     man's enemy.
%  9. An enemy of a persecutor of a servant of a man's father is that 
%     man's friend.
%
%  The Problem is to deduce some facts about the great-grandsons.

% represenation:
%

-Father(x,y) | Master(y,x).
NotSuperior(x,y) | NotUncle(x,z) | -NotOwes(y,z).
-Father(x,y) | -Enemies(y,z) | -Friends(z,w) | NotOwes(x,w).
-Father(x,y) | NotOwes(y,z) | Persecutes(z,x).
NotSuperior(x,y) | -Master(x,z) | -Father(w,z) | Senior(y,w).
-Father(x,y) | -Father(y,z) | -Senior(w,x) | NotUncle(w,z).
-Master(x,y) | NotSuperior(z,x) | -Friends(z,w) | -Enemies(w,t) |
  -Persecutes(t,y).
-Friends(x,y) | NotSuperior(y,z) | -Master(z,w) | -Persecutes(t,w) |
  Enemies(x,t).
-Enemies(x,y) | -Persecutes(y,z) | -Master(w,z) | -Father(w,t) |
  Friends(x,t).

-Father(x,y) | -Father(y,z) | -Father(z,w) | Greatgrandson(x,w).
-Friends(x,y) | Friends(y,x).
-Enemies(x,y) | Enemies(y,x).
-Friends(x,y) | -Enemies(x,y).
Friends(x,y) | Enemies(x,y).
Father(A,B).
Father(B,C).
Father(C,D).
SHAR_EOF
if test -f 'ggson.ver1.in'
then
	echo shar: over-writing existing file "'ggson.ver1.in'"
fi
cat << \SHAR_EOF > 'ggson.ver1.in'
% problem-set/puzzles/carroll/ggson.ver1.in
% created : 07/14/86
% revised : 07/15/88

% description:
%
% This run attempts to solve "The Great-grandson Problem" using
% hyper-resolution, binary resolution, and UR-resolution.
% NO PROOF
%
%    			  THE GREAT-GRANDSON PROBLEM
%
%  1. A man can always master his father.
%  2. An inferior of a man's uncle owes that man money.
%  3. The father of an enemy of a friend of a man owes that man nothing.
%  4. A man is always persecuted by his son's creditors.
%  5. An inferior of the master of a man's son is senior to that man.
%  6. A grandson of a man's junior is not his nephew.
%  7. A servant of an inferior of a friend of a man's enemy is never
%     persecuted by that man.
%  8. A friend of a superior of the master of a man's victim is that
%     man's enemy.
%  9. An enemy of a persecutor of a servant of a man's father is that 
%     man's friend.
%
%  The Problem is to deduce some facts about the great-grandsons.
%                  --- Lewis Carroll from "Symbolic Logic" p362.

% representation:
%

set(hyper_res).
set(binary_res).
set(UR_res).


list(axioms). 

-Father(x,y) | Master(y,x).
NotSuperior(x,y) | NotUncle(x,z) | -NotOwes(y,z).
-Father(x,y) | -Enemies(y,z) | -Friends(z,w) | NotOwes(x,w).
-Father(x,y) | NotOwes(y,z) | Persecutes(z,x).
NotSuperior(x,y) | -Master(x,z) | -Father(w,z) | Senior(y,w).
-Father(x,y) | -Father(y,z) | -Senior(w,x) | NotUncle(w,z).
-Master(x,y) | NotSuperior(z,x) | -Friends(z,w) | -Enemies(w,t) |
  -Persecutes(t,y).
-Friends(x,y) | NotSuperior(y,z) | -Master(z,w) | -Persecutes(t,w) |
  Enemies(x,t).
-Enemies(x,y) | -Persecutes(y,z) | -Master(w,z) | -Father(w,t) |
  Friends(x,t).

-Father(x,y) | -Father(y,z) | -Father(z,w) | Greatgrandson(x,w).
-Friends(x,y) | Friends(y,x).
-Enemies(x,y) | Enemies(y,x).
-Friends(x,y) | -Enemies(x,y).
Friends(x,y) | Enemies(x,y).

end_of_list.


list(sos).

Father(A,B).
Father(B,C).
Father(C,D).

end_of_list.
SHAR_EOF
if test -f 'ggson.ver1.out'
then
	echo shar: over-writing existing file "'ggson.ver1.out'"
fi
cat << \SHAR_EOF > 'ggson.ver1.out'
problem-set/puzzles/carroll/ggson.ver1.out
created : 07/15/88
revised : 07/15/88

OTTER version 0.91, 14 June 1988.

set(hyper_res).
set(binary_res).
set(UR_res).

list(axioms).
1 -Father(x,y) | Master(y,x).
2 NotSuperior(x,y) | NotUncle(x,z) | -NotOwes(y,z).
3 -Father(x,y) | -Enemies(y,z) | -Friends(z,w) | NotOwes(x,w).
4 -Father(x,y) | NotOwes(y,z) | Persecutes(z,x).
5 NotSuperior(x,y) | -Master(x,z) | -Father(w,z) | Senior(y,w).
6 -Father(x,y) | -Father(y,z) | -Senior(w,x) | NotUncle(w,z).
7 -Master(x,y) | NotSuperior(z,x) | -Friends(z,w) | -Enemies(w,t) | -Persecutes(t,y).
8 -Friends(x,y) | NotSuperior(y,z) | -Master(z,w) | -Persecutes(t,w) | Enemies(x,t).
9 -Enemies(x,y) | -Persecutes(y,z) | -Master(w,z) | -Father(w,t) | Friends(x,t).
10 -Father(x,y) | -Father(y,z) | -Father(z,w) | Greatgrandson(x,w).
11 -Friends(x,y) | Friends(y,x).
12 -Enemies(x,y) | Enemies(y,x).
13 -Friends(x,y) | -Enemies(x,y).
14 Friends(x,y) | Enemies(x,y).
end_of_list.

list(sos).
15 Father(A,B).
16 Father(B,C).
17 Father(C,D).
end_of_list.

new given clause: 15 Father(A,B).
** KEPT: 18 (15,10) -Father(x,y) | -Father(y,A) | Greatgrandson(x,B).
** KEPT: 19 (15,10) -Father(x,A) | -Father(B,y) | Greatgrandson(x,y).
** KEPT: 20 (15,10) -Father(B,x) | -Father(x,y) | Greatgrandson(A,y).
** KEPT: 21 (15,6) -Father(x,A) | -Senior(y,x) | NotUncle(y,B).
** KEPT: 22 (15,6) -Father(B,x) | -Senior(y,A) | NotUncle(y,x).
** KEPT: 23 (15,5) NotSuperior(x,y) | -Master(x,B) | Senior(y,A).
** KEPT: 24 (15,4) NotOwes(B,x) | Persecutes(x,A).
** KEPT: 25 (15,3) -Enemies(B,x) | -Friends(x,y) | NotOwes(A,y).
** KEPT: 26 (15,1) Master(B,A).
** KEPT: 27 (15,3,14,14) NotOwes(A,x) | Friends(B,y) | Enemies(y,x).

new given clause: 16 Father(B,C).
** KEPT: 28 (16,10) -Father(x,y) | -Father(y,B) | Greatgrandson(x,C).
** KEPT: 29 (16,10) -Father(x,B) | -Father(C,y) | Greatgrandson(x,y).
** KEPT: 30 (16,10) -Father(C,x) | -Father(x,y) | Greatgrandson(B,y).
** KEPT: 31 (16,6) -Father(x,B) | -Senior(y,x) | NotUncle(y,C).
** KEPT: 32 (16,6) -Father(C,x) | -Senior(y,B) | NotUncle(y,x).
** KEPT: 33 (16,5) NotSuperior(x,y) | -Master(x,C) | Senior(y,B).
** KEPT: 34 (16,4) NotOwes(C,x) | Persecutes(x,B).
** KEPT: 35 (16,3) -Enemies(C,x) | -Friends(x,y) | NotOwes(B,y).
** KEPT: 36 (16,1) Master(C,B).
** KEPT: 37 (16,3,14,14) NotOwes(B,x) | Friends(C,y) | Enemies(y,x).

new given clause: 17 Father(C,D).
** KEPT: 38 (17,10) -Father(x,y) | -Father(y,C) | Greatgrandson(x,D).
** KEPT: 39 (17,10) -Father(x,C) | -Father(D,y) | Greatgrandson(x,y).
** KEPT: 40 (17,10) -Father(D,x) | -Father(x,y) | Greatgrandson(C,y).
** KEPT: 41 (17,6) -Father(x,C) | -Senior(y,x) | NotUncle(y,D).
** KEPT: 42 (17,6) -Father(D,x) | -Senior(y,C) | NotUncle(y,x).
** KEPT: 43 (17,5) NotSuperior(x,y) | -Master(x,D) | Senior(y,C).
** KEPT: 44 (17,4) NotOwes(D,x) | Persecutes(x,C).
** KEPT: 45 (17,3) -Enemies(D,x) | -Friends(x,y) | NotOwes(C,y).
** KEPT: 46 (17,1) Master(D,C).
** KEPT: 47 (17,10,15,16) Greatgrandson(A,D).
** KEPT: 48 (17,3,14,14) NotOwes(C,x) | Friends(D,y) | Enemies(y,x).

new given clause: 26 (15,1) Master(B,A).
** KEPT: 49 (26,9) -Enemies(x,y) | -Persecutes(y,A) | -Father(B,t) | Friends(x,t).
** KEPT: 50 (26,8) -Friends(x,y) | NotSuperior(y,B) | -Persecutes(t,A) | Enemies(x,t).
** KEPT: 51 (26,7) NotSuperior(x,B) | -Friends(x,y) | -Enemies(y,t) | -Persecutes(t,A).
** KEPT: 52 (26,5) NotSuperior(B,x) | -Father(y,A) | Senior(x,y).

new given clause: 36 (16,1) Master(C,B).
** KEPT: 53 (36,9) -Enemies(x,y) | -Persecutes(y,B) | -Father(C,t) | Friends(x,t).
** KEPT: 54 (36,8) -Friends(x,y) | NotSuperior(y,C) | -Persecutes(t,B) | Enemies(x,t).
** KEPT: 55 (36,7) NotSuperior(x,C) | -Friends(x,y) | -Enemies(y,t) | -Persecutes(t,B).
** KEPT: 56 (36,5) NotSuperior(C,x) | -Father(y,B) | Senior(x,y).
** KEPT: 57 (36,5,15) NotSuperior(C,x) | Senior(x,A).

new given clause: 46 (17,1) Master(D,C).
** KEPT: 58 (46,9) -Enemies(x,y) | -Persecutes(y,C) | -Father(D,t) | Friends(x,t).
** KEPT: 59 (46,8) -Friends(x,y) | NotSuperior(y,D) | -Persecutes(t,C) | Enemies(x,t).
** KEPT: 60 (46,7) NotSuperior(x,D) | -Friends(x,y) | -Enemies(y,t) | -Persecutes(t,C).
** KEPT: 61 (46,5) NotSuperior(D,x) | -Father(y,C) | Senior(x,y).
** KEPT: 62 (46,5,16) NotSuperior(D,x) | Senior(x,B).

new given clause: 47 (17,10,15,16) Greatgrandson(A,D).

new given clause: 24 (15,4) NotOwes(B,x) | Persecutes(x,A).
** KEPT: 63 (24,2) Persecutes(x,A) | NotSuperior(y,B) | NotUncle(y,x).
** KEPT: 64 (24,9) NotOwes(B,x) | -Enemies(y,x) | -Master(z,A) | -Father(z,t) | Friends(y,t).
** KEPT: 65 (24,8) NotOwes(B,t) | -Friends(x,y) | NotSuperior(y,z) | -Master(z,A) | Enemies(x,t).
** KEPT: 66 (24,7) NotOwes(B,t) | -Master(x,A) | NotSuperior(y,x) | -Friends(y,z) | -Enemies(z,t).
** KEPT: 67 (24,8,14,26) NotOwes(B,t) | NotSuperior(x,B) | Enemies(y,t) | Enemies(y,x).
** KEPT: 68 (24,7,26,14,14) NotOwes(B,t) | NotSuperior(x,B) | Enemies(x,y) | Friends(y,t).

new given clause: 34 (16,4) NotOwes(C,x) | Persecutes(x,B).
** KEPT: 69 (34,2) Persecutes(x,B) | NotSuperior(y,C) | NotUncle(y,x).
** KEPT: 70 (34,9) NotOwes(C,x) | -Enemies(y,x) | -Master(z,B) | -Father(z,t) | Friends(y,t).
** KEPT: 71 (34,8) NotOwes(C,t) | -Friends(x,y) | NotSuperior(y,z) | -Master(z,B) | Enemies(x,t).
** KEPT: 72 (34,7) NotOwes(C,t) | -Master(x,B) | NotSuperior(y,x) | -Friends(y,z) | -Enemies(z,t).
** KEPT: 73 (34,8,14,36) NotOwes(C,t) | NotSuperior(x,C) | Enemies(y,t) | Enemies(y,x).
** KEPT: 74 (34,7,36,14,14) NotOwes(C,t) | NotSuperior(x,C) | Enemies(x,y) | Friends(y,t).

new given clause: 44 (17,4) NotOwes(D,x) | Persecutes(x,C).
** KEPT: 75 (44,2) Persecutes(x,C) | NotSuperior(y,D) | NotUncle(y,x).
** KEPT: 76 (44,9) NotOwes(D,x) | -Enemies(y,x) | -Master(z,C) | -Father(z,t) | Friends(y,t).
** KEPT: 77 (44,8) NotOwes(D,t) | -Friends(x,y) | NotSuperior(y,z) | -Master(z,C) | Enemies(x,t).
** KEPT: 78 (44,7) NotOwes(D,t) | -Master(x,C) | NotSuperior(y,x) | -Friends(y,z) | -Enemies(z,t).
** KEPT: 79 (44,8,14,46) NotOwes(D,t) | NotSuperior(x,D) | Enemies(y,t) | Enemies(y,x).
** KEPT: 80 (44,7,46,14,14) NotOwes(D,t) | NotSuperior(x,D) | Enemies(x,y) | Friends(y,t).

new given clause: 57 (36,5,15) NotSuperior(C,x) | Senior(x,A).
** KEPT: 81 (57,6) NotSuperior(C,x) | -Father(A,y) | -Father(y,z) | NotUncle(x,z).
** KEPT: 82 (57,6,15,16) NotSuperior(C,x) | NotUncle(x,C).

new given clause: 62 (46,5,16) NotSuperior(D,x) | Senior(x,B).
** KEPT: 83 (62,6) NotSuperior(D,x) | -Father(B,y) | -Father(y,z) | NotUncle(x,z).
** KEPT: 84 (62,6,16,17) NotSuperior(D,x) | NotUncle(x,D).

new given clause: 82 (57,6,15,16) NotSuperior(C,x) | NotUncle(x,C).

new given clause: 84 (62,6,16,17) NotSuperior(D,x) | NotUncle(x,D).

new given clause: 18 (15,10) -Father(x,y) | -Father(y,A) | Greatgrandson(x,B).
** KEPT: 85 (18,17) -Father(D,A) | Greatgrandson(C,B).
** KEPT: 86 (18,16) -Father(C,A) | Greatgrandson(B,B).
** KEPT: 87 (18,15) -Father(B,A) | Greatgrandson(A,B).

new given clause: 85 (18,17) -Father(D,A) | Greatgrandson(C,B).

new given clause: 86 (18,16) -Father(C,A) | Greatgrandson(B,B).

new given clause: 87 (18,15) -Father(B,A) | Greatgrandson(A,B).

new given clause: 19 (15,10) -Father(x,A) | -Father(B,y) | Greatgrandson(x,y).
** KEPT: 88 (19,16) -Father(x,A) | Greatgrandson(x,C).

new given clause: 88 (19,16) -Father(x,A) | Greatgrandson(x,C).

new given clause: 20 (15,10) -Father(B,x) | -Father(x,y) | Greatgrandson(A,y).
** KEPT: 89 (20,16) -Father(C,x) | Greatgrandson(A,x).
** KEPT: 90 (20,16) -Father(B,B) | Greatgrandson(A,C).

new given clause: 89 (20,16) -Father(C,x) | Greatgrandson(A,x).

new given clause: 90 (20,16) -Father(B,B) | Greatgrandson(A,C).

new given clause: 21 (15,6) -Father(x,A) | -Senior(y,x) | NotUncle(y,B).
** KEPT: 91 (21,62) -Father(B,A) | NotUncle(x,B) | NotSuperior(D,x).
** KEPT: 92 (21,57) -Father(A,A) | NotUncle(x,B) | NotSuperior(C,x).
** KEPT: 93 (21,5) -Father(x,A) | NotUncle(y,B) | NotSuperior(z,y) | -Master(z,u) | -Father(x,u).

new given clause: 22 (15,6) -Father(B,x) | -Senior(y,A) | NotUncle(y,x).
** KEPT: 94 (22,16) -Senior(x,A) | NotUncle(x,C).
** KEPT: 95 (22,57) -Father(B,x) | NotUncle(y,x) | NotSuperior(C,y).
** KEPT: 96 (22,5) -Father(B,x) | NotUncle(y,x) | NotSuperior(z,y) | -Master(z,u) | -Father(A,u).

new given clause: 94 (22,16) -Senior(x,A) | NotUncle(x,C).
** KEPT: 97 (94,5) NotUncle(x,C) | NotSuperior(y,x) | -Master(y,z) | -Father(A,z).

new given clause: 23 (15,5) NotSuperior(x,y) | -Master(x,B) | Senior(y,A).
** KEPT: 98 (23,1) NotSuperior(x,y) | Senior(y,A) | -Father(B,x).
** KEPT: 99 (23,94) NotSuperior(x,y) | -Master(x,B) | NotUncle(y,C).
** KEPT: 100 (23,22) NotSuperior(x,y) | -Master(x,B) | -Father(B,z) | NotUncle(y,z).
** KEPT: 101 (23,21) NotSuperior(x,y) | -Master(x,B) | -Father(A,A) | NotUncle(y,B).
** KEPT: 102 (23,6) NotSuperior(x,y) | -Master(x,B) | -Father(A,z) | -Father(z,u) | NotUncle(y,u).

new given clause: 25 (15,3) -Enemies(B,x) | -Friends(x,y) | NotOwes(A,y).
** KEPT: 103 (25,14) -Friends(x,y) | NotOwes(A,y) | Friends(B,x).
** KEPT: 104 (25,12) -Friends(x,y) | NotOwes(A,y) | -Enemies(x,B).
** KEPT: 105 (25,8) -Friends(t,x) | NotOwes(A,x) | -Friends(B,y) | NotSuperior(y,z) | -Master(z,u) | -Persecutes(t,u).
** KEPT: 106 (25,14) -Enemies(B,x) | NotOwes(A,y) | Enemies(x,y).
** KEPT: 107 (25,11) -Enemies(B,x) | NotOwes(A,y) | -Friends(y,x).
** KEPT: 108 (25,9) -Enemies(B,x) | NotOwes(A,t) | -Enemies(x,y) | -Persecutes(y,z) | -Master(u,z) | -Father(u,t).
** KEPT: 109 (25,2) -Enemies(B,x) | -Friends(x,y) | NotSuperior(z,A) | NotUncle(z,y).

new given clause: 27 (15,3,14,14) NotOwes(A,x) | Friends(B,y) | Enemies(y,x).
** KEPT: 110 (27,2) Friends(B,x) | Enemies(x,y) | NotSuperior(z,A) | NotUncle(z,y).
** KEPT: 111 (27,25) NotOwes(A,x) | Enemies(y,x) | -Enemies(B,B) | NotOwes(A,y).
** KEPT: 112 (27,11) NotOwes(A,x) | Enemies(y,x) | Friends(y,B).
** KEPT: 113 (27,8) NotOwes(A,x) | Enemies(y,x) | NotSuperior(y,z) | -Master(z,u) | -Persecutes(t,u) | Enemies(B,t).
** KEPT: 114 (27,7) NotOwes(A,x) | Enemies(y,x) | -Master(z,u) | NotSuperior(B,z) | -Enemies(y,t) | -Persecutes(t,u).
** KEPT: 115 (27,3) NotOwes(A,x) | Enemies(y,x) | -Father(z,u) | -Enemies(u,B) | NotOwes(z,y).
** KEPT: 116 (27,25) NotOwes(A,x) | Friends(B,B) | -Friends(x,y) | NotOwes(A,y).
** KEPT: 117 (27,12) NotOwes(A,x) | Friends(B,y) | Enemies(x,y).
** KEPT: 118 (27,9) NotOwes(A,x) | Friends(B,y) | -Persecutes(x,z) | -Master(u,z) | -Father(u,t) | Friends(y,t).
** KEPT: 119 (27,7) NotOwes(A,t) | Friends(B,x) | -Master(y,z) | NotSuperior(u,y) | -Friends(u,x) | -Persecutes(t,z).
** KEPT: 120 (27,3) NotOwes(A,x) | Friends(B,y) | -Father(z,y) | -Friends(x,u) | NotOwes(z,u).
** KEPT: 121 (27,25,27) NotOwes(A,x) | Enemies(y,x) | NotOwes(A,y) | NotOwes(A,B) | Friends(B,B).
** KEPT: 122 (27,25,14) NotOwes(A,x) | Enemies(y,x) | NotOwes(A,y) | Friends(B,B).
** KEPT: 123 (27,8,46,44) NotOwes(A,x) | Enemies(y,x) | NotSuperior(y,D) | Enemies(B,t) | NotOwes(D,t).
** KEPT: 124 (27,8,36,34) NotOwes(A,x) | Enemies(y,x) | NotSuperior(y,C) | Enemies(B,t) | NotOwes(C,t).
** KEPT: 125 (27,8,26,24) NotOwes(A,x) | Enemies(y,x) | NotSuperior(y,B) | Enemies(B,t) | NotOwes(B,t).
** KEPT: 126 (27,7,46,14,44) NotOwes(A,x) | Enemies(y,x) | NotSuperior(B,D) | Friends(y,t) | NotOwes(D,t).
** KEPT: 127 (27,7,36,14,34) NotOwes(A,x) | Enemies(y,x) | NotSuperior(B,C) | Friends(y,t) | NotOwes(C,t).
** KEPT: 128 (27,7,26,14,24) NotOwes(A,x) | Enemies(y,x) | NotSuperior(B,B) | Friends(y,t) | NotOwes(B,t).
** KEPT: 129 (27,3,17,27) NotOwes(A,x) | Enemies(y,x) | NotOwes(C,y) | NotOwes(A,B) | Friends(B,D).
** KEPT: 130 (27,3,17,14) NotOwes(A,x) | Enemies(y,x) | NotOwes(C,y) | Friends(D,B).
** KEPT: 131 (27,3,16,27) NotOwes(A,x) | Enemies(y,x) | NotOwes(B,y) | NotOwes(A,B) | Friends(B,C).
** KEPT: 132 (27,3,16,14) NotOwes(A,x) | Enemies(y,x) | NotOwes(B,y) | Friends(C,B).
** KEPT: 133 (27,7,46,14,44) NotOwes(A,t) | Friends(B,x) | NotSuperior(y,D) | Enemies(y,x) | NotOwes(D,t).
** KEPT: 134 (27,7,36,14,34) NotOwes(A,t) | Friends(B,x) | NotSuperior(y,C) | Enemies(y,x) | NotOwes(C,t).
** KEPT: 135 (27,7,26,14,24) NotOwes(A,t) | Friends(B,x) | NotSuperior(y,B) | Enemies(y,x) | NotOwes(B,t).
** KEPT: 136 (27,3,17,14) NotOwes(A,x) | Friends(B,D) | NotOwes(C,y) | Enemies(x,y).
** KEPT: 137 (27,3,16,14) NotOwes(A,x) | Friends(B,C) | NotOwes(B,y) | Enemies(x,y).
122 back subsumes: 121 (27,25,27) NotOwes(A,x) | Enemies(y,x) | NotOwes(A,y) | NotOwes(A,B) | Friends(B,B).

new given clause: 28 (16,10) -Father(x,y) | -Father(y,B) | Greatgrandson(x,C).
** KEPT: 138 (28,17) -Father(D,B) | Greatgrandson(C,C).
** KEPT: 139 (28,16) -Father(C,B) | Greatgrandson(B,C).

new given clause: 138 (28,17) -Father(D,B) | Greatgrandson(C,C).

new given clause: 139 (28,16) -Father(C,B) | Greatgrandson(B,C).

new given clause: 29 (16,10) -Father(x,B) | -Father(C,y) | Greatgrandson(x,y).
** KEPT: 140 (29,17) -Father(x,B) | Greatgrandson(x,D).

new given clause: 140 (29,17) -Father(x,B) | Greatgrandson(x,D).

new given clause: 30 (16,10) -Father(C,x) | -Father(x,y) | Greatgrandson(B,y).
** KEPT: 141 (30,17) -Father(D,x) | Greatgrandson(B,x).
** KEPT: 142 (30,17) -Father(C,C) | Greatgrandson(B,D).

new given clause: 141 (30,17) -Father(D,x) | Greatgrandson(B,x).

new given clause: 142 (30,17) -Father(C,C) | Greatgrandson(B,D).

new given clause: 31 (16,6) -Father(x,B) | -Senior(y,x) | NotUncle(y,C).
** KEPT: 143 (31,62) -Father(B,B) | NotUncle(x,C) | NotSuperior(D,x).
** KEPT: 144 (31,5) -Father(x,B) | NotUncle(y,C) | NotSuperior(z,y) | -Master(z,u) | -Father(x,u).

new given clause: 32 (16,6) -Father(C,x) | -Senior(y,B) | NotUncle(y,x).
** KEPT: 145 (32,17) -Senior(x,B) | NotUncle(x,D).
** KEPT: 146 (32,62) -Father(C,x) | NotUncle(y,x) | NotSuperior(D,y).
** KEPT: 147 (32,5) -Father(C,x) | NotUncle(y,x) | NotSuperior(z,y) | -Master(z,u) | -Father(B,u).

new given clause: 145 (32,17) -Senior(x,B) | NotUncle(x,D).
** KEPT: 148 (145,5) NotUncle(x,D) | NotSuperior(y,x) | -Master(y,z) | -Father(B,z).

new given clause: 33 (16,5) NotSuperior(x,y) | -Master(x,C) | Senior(y,B).
** KEPT: 149 (33,1) NotSuperior(x,y) | Senior(y,B) | -Father(C,x).
** KEPT: 150 (33,145) NotSuperior(x,y) | -Master(x,C) | NotUncle(y,D).
** KEPT: 151 (33,32) NotSuperior(x,y) | -Master(x,C) | -Father(C,z) | NotUncle(y,z).
** KEPT: 152 (33,31) NotSuperior(x,y) | -Master(x,C) | -Father(B,B) | NotUncle(y,C).
** KEPT: 153 (33,21) NotSuperior(x,y) | -Master(x,C) | -Father(B,A) | NotUncle(y,B).
** KEPT: 154 (33,6) NotSuperior(x,y) | -Master(x,C) | -Father(B,z) | -Father(z,u) | NotUncle(y,u).

new given clause: 35 (16,3) -Enemies(C,x) | -Friends(x,y) | NotOwes(B,y).
** KEPT: 155 (35,27) -Friends(x,y) | NotOwes(B,y) | NotOwes(A,x) | Friends(B,C).
** KEPT: 156 (35,14) -Friends(x,y) | NotOwes(B,y) | Friends(C,x).
** KEPT: 157 (35,12) -Friends(x,y) | NotOwes(B,y) | -Enemies(x,C).
** KEPT: 158 (35,8) -Friends(t,x) | NotOwes(B,x) | -Friends(C,y) | NotSuperior(y,z) | -Master(z,u) | -Persecutes(t,u).
** KEPT: 159 (35,27) -Enemies(C,B) | NotOwes(B,x) | NotOwes(A,y) | Enemies(x,y).
** KEPT: 160 (35,14) -Enemies(C,x) | NotOwes(B,y) | Enemies(x,y).
** KEPT: 161 (35,11) -Enemies(C,x) | NotOwes(B,y) | -Friends(y,x).
** KEPT: 162 (35,9) -Enemies(C,x) | NotOwes(B,t) | -Enemies(x,y) | -Persecutes(y,z) | -Master(u,z) | -Father(u,t).
** KEPT: 163 (35,2) -Enemies(C,x) | -Friends(x,y) | NotSuperior(z,B) | NotUncle(z,y).

new given clause: 37 (16,3,14,14) NotOwes(B,x) | Friends(C,y) | Enemies(y,x).
SHAR_EOF
if test -f 'letters.desc'
then
	echo shar: over-writing existing file "'letters.desc'"
fi
cat << \SHAR_EOF > 'letters.desc'
 problem-set/puzzles/carroll/letters.desc
 created : 07/19/88
 revised : 07/19/88 

 Natural Language Description:

 This run solves "The Letters Puzzle" using
 UR-resolution, hyper-resolution, and binary resolution.     

                		The Letters Puzzle

 (1) All the dated letters in this room are written on blue paper.
 (2) None of them are in black ink, except those that are written
     in the third person.
 (3) I have not filed any of them that I can read.
 (4) None of them, that are written on one sheet, are undated.
 (5) All of them, that are not crossed, are in black ink.
 (6) All of them, written by Brown, begin with "Dear Sir."
 (7) All of them, written on blue paper, are filed.
 (8) None of them,  written on more than one sheet, are crossed.
 (9) None of them, that begin with "Dear Sir," are written in
     third person.
     Find out everything that you can about the letters.
					-Lewis Carroll, Symbolic Logic, p. 175 

Versions:

letters.ver1.in : uses hyper-resolution, binary-resolution, and 
	UR-resolution. Answer: I cannot read any of Brown's letters.     

		created by : Kelly Ratliff
		verifed for ITP : unverified
		translated for OTTER by : K.R.
		verified for OTTER : 07/19/88
SHAR_EOF
if test -f 'letters.ver1.clauses'
then
	echo shar: over-writing existing file "'letters.ver1.clauses'"
fi
cat << \SHAR_EOF > 'letters.ver1.clauses'
% problem-set/puzzles/carroll/letters.ver1.clauses 
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Letters Puzzle" using
% UR-resolution, hyper-resolution, and binary resolution.     
%
%                		The Letters Puzzle
%
% (1) All the dated letters in this room are written on blue paper.
% (2) None of them are in black ink, except those that are written
%     in the third person.
% (3) I have not filed any of them that I can read.
% (4) None of them, that are written on one sheet, are undated.
% (5) All of them, that are not crossed, are in black ink.
% (6) All of them, written by Brown, begin with "Dear Sir."
% (7) All of them, written on blue paper, are filed.
% (8) None of them,  written on more than one sheet, are crossed.
% (9) None of them, that begin with "Dear Sir," are written in
%     third person.
%     Find out everything that you can about the letters.
%						-Lewis Carroll, Symbolic Logic, p. 175 

% representation:
%
                  

-DATED | ON_BLUE_PAPER.
-IN_THIRD_PERSON | IN_BLACK_INK.
IN_THIRD_PERSON | -IN_BLACK_INK.
-CAN_BE_READ | -FILED.
-ON_ONE_SHEET | DATED.
CROSSED | IN_BLACK_INK.
-BY_BROWN | BEGINS_WITH_DEAR_SIR.
-ON_BLUE_PAPER | FILED.
ON_ONE_SHEET | -CROSSED.
-BEGINS_WITH_DEAR_SIR | -IN_THIRD_PERSON.
SHAR_EOF
if test -f 'letters.ver1.in'
then
	echo shar: over-writing existing file "'letters.ver1.in'"
fi
cat << \SHAR_EOF > 'letters.ver1.in'
% problem-set/puzzles/carroll/letters.ver1.in
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Letters Puzzle" using
% UR-resolution, hyper-resolution, and binary resolution.     
%
%                		The Letters Puzzle
%
% (1) All the dated letters in this room are written on blue paper.
% (2) None of them are in black ink, except those that are written
%     in the third person.
% (3) I have not filed any of them that I can read.
% (4) None of them, that are written on one sheet, are undated.
% (5) All of them, that are not crossed, are in black ink.
% (6) All of them, written by Brown, begin with "Dear Sir."
% (7) All of them, written on blue paper, are filed.
% (8) None of them,  written on more than one sheet, are crossed.
% (9) None of them, that begin with "Dear Sir," are written in
%     third person.
%     Find out everything that you can about the letters.
%						-Lewis Carroll, Symbolic Logic, p. 175 

% representation:
%
                  
set(hyper_res).
set(UR_res).
set(binary_res).


list(sos).

-DATED | ON_BLUE_PAPER.
-IN_THIRD_PERSON | IN_BLACK_INK.
IN_THIRD_PERSON | -IN_BLACK_INK.
-CAN_BE_READ | -FILED.
-ON_ONE_SHEET | DATED.
CROSSED | IN_BLACK_INK.
-BY_BROWN | BEGINS_WITH_DEAR_SIR.
-ON_BLUE_PAPER | FILED.
ON_ONE_SHEET | -CROSSED.
-BEGINS_WITH_DEAR_SIR | -IN_THIRD_PERSON.

end_of_list.
SHAR_EOF
if test -f 'letters.ver1.out'
then
	echo shar: over-writing existing file "'letters.ver1.out'"
fi
cat << \SHAR_EOF > 'letters.ver1.out'
problem-set/puzzles/carroll/letters.ver1.out
created : 07/19/88
revised : 07/19/88

OTTER version 0.91, 14 June 1988.

set(hyper_res).
set(UR_res).
set(binary_res).

list(sos).
1 -DATED | ON_BLUE_PAPER.
2 -IN_THIRD_PERSON | IN_BLACK_INK.
3 IN_THIRD_PERSON | -IN_BLACK_INK.
4 -CAN_BE_READ | -FILED.
5 -ON_ONE_SHEET | DATED.
6 CROSSED | IN_BLACK_INK.
7 -BY_BROWN | BEGINS_WITH_DEAR_SIR.
8 -ON_BLUE_PAPER | FILED.
9 ON_ONE_SHEET | -CROSSED.
10 -BEGINS_WITH_DEAR_SIR | -IN_THIRD_PERSON.
end_of_list.

new given clause: 1 -DATED | ON_BLUE_PAPER.

new given clause: 2 -IN_THIRD_PERSON | IN_BLACK_INK.

new given clause: 3 IN_THIRD_PERSON | -IN_BLACK_INK.

new given clause: 4 -CAN_BE_READ | -FILED.

new given clause: 5 -ON_ONE_SHEET | DATED.
** KEPT: 11 (5,1) -ON_ONE_SHEET | ON_BLUE_PAPER.

new given clause: 6 CROSSED | IN_BLACK_INK.
** KEPT: 12 (6,3) CROSSED | IN_THIRD_PERSON.

new given clause: 7 -BY_BROWN | BEGINS_WITH_DEAR_SIR.

new given clause: 8 -ON_BLUE_PAPER | FILED.
** KEPT: 13 (8,1) FILED | -DATED.
** KEPT: 14 (8,4) -ON_BLUE_PAPER | -CAN_BE_READ.

new given clause: 9 ON_ONE_SHEET | -CROSSED.
** KEPT: 15 (9,5) -CROSSED | DATED.
** KEPT: 16 (9,6) ON_ONE_SHEET | IN_BLACK_INK.

new given clause: 10 -BEGINS_WITH_DEAR_SIR | -IN_THIRD_PERSON.
** KEPT: 17 (10,7) -IN_THIRD_PERSON | -BY_BROWN.
** KEPT: 18 (10,3) -BEGINS_WITH_DEAR_SIR | -IN_BLACK_INK.

new given clause: 11 (5,1) -ON_ONE_SHEET | ON_BLUE_PAPER.
** KEPT: 19 (11,9) ON_BLUE_PAPER | -CROSSED.
** KEPT: 20 (11,8) -ON_ONE_SHEET | FILED.

new given clause: 12 (6,3) CROSSED | IN_THIRD_PERSON.
** KEPT: 21 (12,9) IN_THIRD_PERSON | ON_ONE_SHEET.
** KEPT: 22 (12,10) CROSSED | -BEGINS_WITH_DEAR_SIR.

new given clause: 13 (8,1) FILED | -DATED.
** KEPT: 23 (13,4) -DATED | -CAN_BE_READ.

new given clause: 14 (8,4) -ON_BLUE_PAPER | -CAN_BE_READ.
** KEPT: 24 (14,11) -CAN_BE_READ | -ON_ONE_SHEET.

new given clause: 15 (9,5) -CROSSED | DATED.
** KEPT: 25 (15,12) DATED | IN_THIRD_PERSON.
** KEPT: 26 (15,6) DATED | IN_BLACK_INK.
** KEPT: 27 (15,13) -CROSSED | FILED.

new given clause: 16 (9,6) ON_ONE_SHEET | IN_BLACK_INK.
** KEPT: 28 (16,11) IN_BLACK_INK | ON_BLUE_PAPER.

new given clause: 17 (10,7) -IN_THIRD_PERSON | -BY_BROWN.
** KEPT: 29 (17,12) -BY_BROWN | CROSSED.
** KEPT: 30 (17,3) -BY_BROWN | -IN_BLACK_INK.

new given clause: 18 (10,3) -BEGINS_WITH_DEAR_SIR | -IN_BLACK_INK.
** KEPT: 31 (18,16) -BEGINS_WITH_DEAR_SIR | ON_ONE_SHEET.

new given clause: 19 (11,9) ON_BLUE_PAPER | -CROSSED.
** KEPT: 32 (19,14) -CROSSED | -CAN_BE_READ.
** KEPT: 33 (19,12) ON_BLUE_PAPER | IN_THIRD_PERSON.

new given clause: 20 (11,8) -ON_ONE_SHEET | FILED.
** KEPT: 34 (20,16) FILED | IN_BLACK_INK.

new given clause: 21 (12,9) IN_THIRD_PERSON | ON_ONE_SHEET.
** KEPT: 35 (21,17) ON_ONE_SHEET | -BY_BROWN.
** KEPT: 36 (21,20) IN_THIRD_PERSON | FILED.

new given clause: 22 (12,10) CROSSED | -BEGINS_WITH_DEAR_SIR.
** KEPT: 37 (22,19) -BEGINS_WITH_DEAR_SIR | ON_BLUE_PAPER.
** KEPT: 38 (22,15) -BEGINS_WITH_DEAR_SIR | DATED.

new given clause: 23 (13,4) -DATED | -CAN_BE_READ.

new given clause: 24 (14,11) -CAN_BE_READ | -ON_ONE_SHEET.
** KEPT: 39 (24,21) -CAN_BE_READ | IN_THIRD_PERSON.
** KEPT: 40 (24,16) -CAN_BE_READ | IN_BLACK_INK.

new given clause: 25 (15,12) DATED | IN_THIRD_PERSON.
** KEPT: 41 (25,17) DATED | -BY_BROWN.

new given clause: 26 (15,6) DATED | IN_BLACK_INK.

new given clause: 27 (15,13) -CROSSED | FILED.
** KEPT: 42 (27,22) FILED | -BEGINS_WITH_DEAR_SIR.

new given clause: 28 (16,11) IN_BLACK_INK | ON_BLUE_PAPER.

new given clause: 29 (17,12) -BY_BROWN | CROSSED.
** KEPT: 43 (29,27) -BY_BROWN | FILED.
** KEPT: 44 (29,19) -BY_BROWN | ON_BLUE_PAPER.

new given clause: 30 (17,3) -BY_BROWN | -IN_BLACK_INK.

new given clause: 31 (18,16) -BEGINS_WITH_DEAR_SIR | ON_ONE_SHEET.
** KEPT: 45 (31,24) -BEGINS_WITH_DEAR_SIR | -CAN_BE_READ.

new given clause: 32 (19,14) -CROSSED | -CAN_BE_READ.
** KEPT: 46 (32,29) -CAN_BE_READ | -BY_BROWN.

new given clause: 33 (19,12) ON_BLUE_PAPER | IN_THIRD_PERSON.

new given clause: 34 (20,16) FILED | IN_BLACK_INK.

new given clause: 35 (21,17) ON_ONE_SHEET | -BY_BROWN.

new given clause: 36 (21,20) IN_THIRD_PERSON | FILED.

new given clause: 37 (22,19) -BEGINS_WITH_DEAR_SIR | ON_BLUE_PAPER.

new given clause: 38 (22,15) -BEGINS_WITH_DEAR_SIR | DATED.

new given clause: 39 (24,21) -CAN_BE_READ | IN_THIRD_PERSON.

new given clause: 40 (24,16) -CAN_BE_READ | IN_BLACK_INK.

new given clause: 41 (25,17) DATED | -BY_BROWN.

new given clause: 42 (27,22) FILED | -BEGINS_WITH_DEAR_SIR.

new given clause: 43 (29,27) -BY_BROWN | FILED.

new given clause: 44 (29,19) -BY_BROWN | ON_BLUE_PAPER.

new given clause: 45 (31,24) -BEGINS_WITH_DEAR_SIR | -CAN_BE_READ.

new given clause: 46 (32,29) -CAN_BE_READ | -BY_BROWN.

------------ END OF SEARCH ------------

sos empty.

--------------- options ---------------
set(binary_res).
set(hyper_res).
set(UR_res).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
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                 10
clauses given                 46
clauses generated            160
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            2
clauses forward subsumed     122
(clauses subsumed by sos)    106
unit deletions                 0
clauses kept                  36
empty clauses                  0
factors generated              0
clauses back subsumed          0
clauses not processed          0

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

Natural Language Description:

                  		The Animals

 (1)  All cunning savage animals are destructive.
 (2)  No fat lazy animals climb trees.
 (3)  All poisonous animals with claws wriggle.
 (4)  No lizards are destructive unless they climb trees.
 (5)  All animals, that have claws but no scales, are fat.
 (6)  All grinning animals, that are dreaded, have claws.
 (7)  No active destructive animal is fat.
 (8)  All animals with scales, that are dreaded, are poisonous.
 (9)  All grinning animals with claws are cunning.
 (10) No savage lizard is viewed without dread.
 (11) A savage lizard is an object of dread.
      Deduce everything you can about these animals.
                        -Lewis Carroll, Symbolic Logic, p.408

Versions : 

lizard.ver1.in : Uses hyper-resolution, UR-resolution, and 
	binary-resolution.

		created by : Kelly Ratliff
		verified for ITP : unverified
		translated for OTTER by : K.R.
		verified for OTTER : 07/19/88
SHAR_EOF
if test -f 'lizard.ver1.clauses'
then
	echo shar: over-writing existing file "'lizard.ver1.clauses'"
fi
cat << \SHAR_EOF > 'lizard.ver1.clauses'
% problem-set/puzzles/carroll/lizard.ver1.clauses  
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Animals Puzzle" by using UR-resolution,
% hyper-resolution, and binary resolution.     
%
%                   		The Animals
%
%  (1)  All cunning savage animals are destructive.
%  (2)  No fat lazy animals climb trees.
%  (3)  All poisonous animals with claws wriggle.
%  (4)  No lizards are destructive unless they climb trees.
%  (5)  All animals, that have claws but no scales, are fat.
%  (6)  All grinning animals, that are dreaded, have claws.
%  (7)  No active destructive animal is fat.
%  (8)  All animals with scales, that are dreaded, are poisonous.
%  (9)  All grinning animals with claws are cunning.
%  (10) No savage lizard is viewed without dread.
%  (11) A savage lizard is an object of dread.
%       Deduce everything you can about these animals.
%                         -Lewis Carroll, Symbolic Logic, p.408

% representation:
%
                  

-CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x).
-FAT(x) | -LAZY(x) | -CLIMB_TREES(x).
-POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x).
-CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x).
CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x).
-HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x).
-GRINNING(x) | -DREADED(x) | HAS_CLAWS(x).
-ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x). 
-HAS_SCALES(x) | -DREADED(x) | POISONOUS(x).
-GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x).
-SAVAGE(x) | -LIZARD(x) | DREADED(x).
SHAR_EOF
if test -f 'lizard.ver1.in'
then
	echo shar: over-writing existing file "'lizard.ver1.in'"
fi
cat << \SHAR_EOF > 'lizard.ver1.in'
% problem-set/puzzles/carroll/lizard.ver1.in 
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Animals Puzzle" by using UR-resolution,
% hyper-resolution, and binary resolution.     
%
%                   		The Animals
%
%  (1)  All cunning savage animals are destructive.
%  (2)  No fat lazy animals climb trees.
%  (3)  All poisonous animals with claws wriggle.
%  (4)  No lizards are destructive unless they climb trees.
%  (5)  All animals, that have claws but no scales, are fat.
%  (6)  All grinning animals, that are dreaded, have claws.
%  (7)  No active destructive animal is fat.
%  (8)  All animals with scales, that are dreaded, are poisonous.
%  (9)  All grinning animals with claws are cunning.
%  (10) No savage lizard is viewed without dread.
%  (11) A savage lizard is an object of dread.
%       Deduce everything you can about these animals.
%                         -Lewis Carroll, Symbolic Logic, p.408

% representation:
%
                  
set(hyper_res).
set(UR_res).
set(binary_res).


list(sos).

-CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x).
-FAT(x) | -LAZY(x) | -CLIMB_TREES(x).
-POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x).
-CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x).
CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x).
-HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x).
-GRINNING(x) | -DREADED(x) | HAS_CLAWS(x).
-ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x). 
-HAS_SCALES(x) | -DREADED(x) | POISONOUS(x).
-GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x).
-SAVAGE(x) | -LIZARD(x) | DREADED(x).

end_of_list.
SHAR_EOF
if test -f 'lizard.ver1.out'
then
	echo shar: over-writing existing file "'lizard.ver1.out'"
fi
cat << \SHAR_EOF > 'lizard.ver1.out'
problem-set/puzzles/carroll/lizard.ver1.out
created : 07/19/88
revised : 07/19/88

OTTER version 0.91, 14 June 1988.

set(hyper_res).
set(UR_res).
set(binary_res).

list(sos).
12 -CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x).
13 -FAT(x) | -LAZY(x) | -CLIMB_TREES(x).
14 -POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x).
15 -CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x).
16 CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x).
17 -HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x).
18 -GRINNING(x) | -DREADED(x) | HAS_CLAWS(x).
19 -ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x).
20 -HAS_SCALES(x) | -DREADED(x) | POISONOUS(x).
21 -GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x).
22 -SAVAGE(x) | -LIZARD(x) | DREADED(x).
end_of_list.

new given clause: 12 -CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x).
** KEPT: 23 (12,10) -SAVAGE(x) | DESTRUCTIVE(x) | -GRINNING(x) | -HAS_CLAWS(x).
** KEPT: 24 (12,8) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -FAT(x).
** KEPT: 25 (12,5) -CUNNING(x) | -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x).

new given clause: 13 -FAT(x) | -LAZY(x) | -CLIMB_TREES(x).
** KEPT: 26 (13,6) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | HAS_SCALES(x).
** KEPT: 27 (13,5) -FAT(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 14 -POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x).
** KEPT: 28 (14,9) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x).
** KEPT: 29 (14,7) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -DREADED(x).

new given clause: 15 -CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x).
** KEPT: 30 (15,8) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x).

new given clause: 16 CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 17 -HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x).
** KEPT: 31 (17,7) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 32 (17,9) -HAS_CLAWS(x) | FAT(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 33 (17,8) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 18 -GRINNING(x) | -DREADED(x) | HAS_CLAWS(x).
** KEPT: 34 (18,11) -GRINNING(x) | HAS_CLAWS(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 35 (18,10) -GRINNING(x) | -DREADED(x) | CUNNING(x).

new given clause: 19 -ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x).

new given clause: 20 -HAS_SCALES(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 36 (20,11) -HAS_SCALES(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 21 -GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x).

new given clause: 22 -SAVAGE(x) | -LIZARD(x) | DREADED(x).

new given clause: 35 (18,10) -GRINNING(x) | -DREADED(x) | CUNNING(x).
** KEPT: 37 (35,22) -GRINNING(x) | CUNNING(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 38 (35,12) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | DESTRUCTIVE(x).

new given clause: 23 (12,10) -SAVAGE(x) | DESTRUCTIVE(x) | -GRINNING(x) | -HAS_CLAWS(x).
** KEPT: 39 (23,19) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -FAT(x).
** KEPT: 40 (23,16) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | CLIMB_TREES(x) | -LIZARD(x).

new given clause: 24 (12,8) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -FAT(x).
** KEPT: 41 (24,35) -SAVAGE(x) | -ACTIVE(x) | -FAT(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 42 (24,17) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x).

new given clause: 25 (12,5) -CUNNING(x) | -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x).
** KEPT: 43 (25,35) -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 44 (25,13) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x).

new given clause: 26 (13,6) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | HAS_SCALES(x).
** KEPT: 45 (26,25) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -CUNNING(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 46 (26,16) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 47 (26,18) -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 48 (26,20) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x).

new given clause: 27 (13,5) -FAT(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 49 (27,23) -FAT(x) | -LAZY(x) | -LIZARD(x) | -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x).

new given clause: 28 (14,9) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x).
** KEPT: 50 (28,18) WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x) | -GRINNING(x).
** KEPT: 51 (28,26) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -CLIMB_TREES(x).
** KEPT: 52 (28,17) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | FAT(x).
** KEPT: 53 (28,22) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 29 (14,7) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 54 (29,22) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 30 (15,8) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x).
** KEPT: 55 (30,17) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x).

new given clause: 31 (17,7) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 56 (31,20) FAT(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 57 (31,30) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).
** KEPT: 58 (31,27) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 59 (31,24) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).
** KEPT: 60 (31,19) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 61 (31,22) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 32 (17,9) -HAS_CLAWS(x) | FAT(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 62 (32,30) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).
** KEPT: 63 (32,27) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 64 (32,24) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).
** KEPT: 65 (32,19) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 66 (32,22) -HAS_CLAWS(x) | FAT(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 33 (17,8) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 67 (33,28) -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | WRIGGLES(x) | -DREADED(x).
** KEPT: 68 (33,23) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x).

new given clause: 34 (18,11) -GRINNING(x) | HAS_CLAWS(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 69 (34,33) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 70 (34,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x).
** KEPT: 71 (34,23) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | DESTRUCTIVE(x).

new given clause: 36 (20,11) -HAS_SCALES(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 72 (36,33) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 73 (36,26) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x).

new given clause: 37 (35,22) -GRINNING(x) | CUNNING(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 74 (37,25) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | CLIMB_TREES(x).
** KEPT: 75 (37,24) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x).
74 back subsumes: 43 (25,35) -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x) | -GRINNING(x) | -DREADED(x).
74 back subsumes: 40 (23,16) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | CLIMB_TREES(x) | -LIZARD(x).

new given clause: 38 (35,12) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | DESTRUCTIVE(x).
** KEPT: 76 (38,27) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -FAT(x) | -LAZY(x) | -LIZARD(x).

new given clause: 50 (28,18) WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x) | -GRINNING(x).
** KEPT: 77 (50,31) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | FAT(x).
** KEPT: 78 (50,22) WRIGGLES(x) | -HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 52 (28,17) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | FAT(x).
** KEPT: 79 (52,22) -HAS_CLAWS(x) | WRIGGLES(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 80 (52,30) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).
** KEPT: 81 (52,27) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 82 (52,24) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).

new given clause: 56 (31,20) FAT(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 83 (56,30) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).
** KEPT: 84 (56,27) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 85 (56,24) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).
** KEPT: 86 (56,19) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 87 (56,13) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x).
** KEPT: 88 (56,22) FAT(x) | -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 71 (34,23) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | DESTRUCTIVE(x).
** KEPT: 89 (71,27) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x).
89 back subsumes: 76 (38,27) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -FAT(x) | -LAZY(x) | -LIZARD(x).
89 back subsumes: 49 (27,23) -FAT(x) | -LAZY(x) | -LIZARD(x) | -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x).

new given clause: 74 (37,25) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | CLIMB_TREES(x).
** KEPT: 90 (74,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x).

new given clause: 77 (50,31) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | FAT(x).
** KEPT: 91 (77,22) WRIGGLES(x) | -GRINNING(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 92 (77,30) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).
** KEPT: 93 (77,27) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 94 (77,24) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).
** KEPT: 95 (77,19) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 96 (77,13) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -CLIMB_TREES(x).

new given clause: 39 (23,19) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -FAT(x).
** KEPT: 97 (39,77) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | WRIGGLES(x) | -DREADED(x).
** KEPT: 98 (39,56) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DREADED(x) | POISONOUS(x).

new given clause: 41 (24,35) -SAVAGE(x) | -ACTIVE(x) | -FAT(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 99 (41,77) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | WRIGGLES(x).
** KEPT: 100 (41,56) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 101 (41,31) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | HAS_SCALES(x).
99 back subsumes: 97 (39,77) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | WRIGGLES(x) | -DREADED(x).
99 back subsumes: 94 (77,24) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).
100 back subsumes: 98 (39,56) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DREADED(x) | POISONOUS(x).
100 back subsumes: 85 (56,24) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).
101 back subsumes: 59 (31,24) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).

new given clause: 42 (24,17) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x).
** KEPT: 102 (42,34) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -LIZARD(x).
** KEPT: 103 (42,36) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -LIZARD(x).

new given clause: 44 (25,13) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x).
** KEPT: 104 (44,77) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x) | -GRINNING(x).
** KEPT: 105 (44,56) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 106 (44,52) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x).
** KEPT: 107 (44,32) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 108 (44,31) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x).

new given clause: 46 (26,16) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x).
** KEPT: 109 (46,34) -LAZY(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x) | -GRINNING(x) | -SAVAGE(x).
** KEPT: 110 (46,36) -LAZY(x) | -HAS_CLAWS(x) | -LIZARD(x) | -DESTRUCTIVE(x) | POISONOUS(x) | -SAVAGE(x).

new given clause: 47 (26,18) -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x).
** KEPT: 111 (47,74) -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -LIZARD(x).
111 back subsumes: 108 (44,31) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x).

new given clause: 48 (26,20) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x).
** KEPT: 112 (48,74) -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 51 (28,26) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -CLIMB_TREES(x).
** KEPT: 113 (51,22) -HAS_CLAWS(x) | WRIGGLES(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 114 (51,74) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 53 (28,22) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 115 (53,46) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x).
** KEPT: 116 (53,42) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -ACTIVE(x).
** KEPT: 117 (53,33) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 54 (29,22) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 55 (30,17) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x).
** KEPT: 118 (55,34) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x).
** KEPT: 119 (55,53) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x).
** KEPT: 120 (55,36) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x).

new given clause: 60 (31,19) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 61 (31,22) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 121 (61,44) HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).

new given clause: 65 (32,19) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 66 (32,22) -HAS_CLAWS(x) | FAT(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 122 (66,44) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).
** KEPT: 123 (66,39) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -GRINNING(x) | -ACTIVE(x).
122 back subsumes: 107 (44,32) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x).

new given clause: 67 (33,28) -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | WRIGGLES(x) | -DREADED(x).

new given clause: 68 (33,23) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x).
** KEPT: 124 (68,34) HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | -LIZARD(x).
** KEPT: 125 (68,53) -HAS_CLAWS(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | WRIGGLES(x) | -LIZARD(x).
124 back subsumes: 118 (55,34) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x).
124 back subsumes: 102 (42,34) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -LIZARD(x).
124 back subsumes: 69 (34,33) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 75 (37,24) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x).

new given clause: 78 (50,22) WRIGGLES(x) | -HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 79 (52,22) -HAS_CLAWS(x) | WRIGGLES(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 126 (79,44) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).
126 back subsumes: 106 (44,52) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x).

new given clause: 86 (56,19) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x).
** KEPT: 127 (86,22) -GRINNING(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 87 (56,13) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x).
** KEPT: 128 (87,22) -GRINNING(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 129 (87,74) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -SAVAGE(x) | -LIZARD(x).
129 back subsumes: 112 (48,74) -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).
129 back subsumes: 105 (44,56) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x).

new given clause: 88 (56,22) FAT(x) | -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 130 (88,75) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x).
** KEPT: 131 (88,44) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).
** KEPT: 132 (88,27) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x).
130 back subsumes: 127 (86,22) -GRINNING(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | -SAVAGE(x) | -LIZARD(x).
130 back subsumes: 123 (66,39) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -GRINNING(x) | -ACTIVE(x).

new given clause: 89 (71,27) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x).
** KEPT: 133 (89,88) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | POISONOUS(x).
** KEPT: 134 (89,79) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x).
** KEPT: 135 (89,77) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x).
** KEPT: 136 (89,61) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x).
133 back subsumes: 132 (88,27) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x).
133 back subsumes: 131 (88,44) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).
133 back subsumes: 129 (87,74) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -SAVAGE(x) | -LIZARD(x).
133 back subsumes: 128 (87,22) -GRINNING(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x).
134 back subsumes: 114 (51,74) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x).
135 back subsumes: 104 (44,77) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x) | -GRINNING(x).
136 back subsumes: 121 (61,44) HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).
136 back subsumes: 111 (47,74) -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -LIZARD(x).
136 back subsumes: 109 (46,34) -LAZY(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x) | -GRINNING(x) | -SAVAGE(x).
136 back subsumes: 90 (74,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x).
136 back subsumes: 70 (34,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x).

new given clause: 91 (77,22) WRIGGLES(x) | -GRINNING(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x).
** KEPT: 137 (91,89) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x).
** KEPT: 138 (91,75) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x).
137 back subsumes: 135 (89,77) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x).
137 back subsumes: 134 (89,79) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x).
138 back subsumes: 125 (68,53) -HAS_CLAWS(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | WRIGGLES(x) | -LIZARD(x).

new given clause: 95 (77,19) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 96 (77,13) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -CLIMB_TREES(x).

new given clause: 99 (41,77) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | WRIGGLES(x).

new given clause: 100 (41,56) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x).

new given clause: 101 (41,31) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | HAS_SCALES(x).

new given clause: 124 (68,34) HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | -LIZARD(x).

new given clause: 130 (88,75) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 133 (89,88) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | POISONOUS(x).

new given clause: 136 (89,61) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x).

new given clause: 137 (91,89) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x).

new given clause: 138 (91,75) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 45 (26,25) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -CUNNING(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 57 (31,30) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 58 (31,27) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 62 (32,30) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 63 (32,27) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 64 (32,24) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).

new given clause: 72 (36,33) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 73 (36,26) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x).

new given clause: 80 (52,30) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 81 (52,27) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 82 (52,24) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x).

new given clause: 83 (56,30) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 84 (56,27) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 92 (77,30) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x).

new given clause: 93 (77,27) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x).

new given clause: 103 (42,36) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -LIZARD(x).

new given clause: 110 (46,36) -LAZY(x) | -HAS_CLAWS(x) | -LIZARD(x) | -DESTRUCTIVE(x) | POISONOUS(x) | -SAVAGE(x).

new given clause: 113 (51,22) -HAS_CLAWS(x) | WRIGGLES(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x).

new given clause: 115 (53,46) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x).

new given clause: 116 (53,42) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -ACTIVE(x).

new given clause: 117 (53,33) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -DESTRUCTIVE(x).

new given clause: 119 (55,53) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x).

new given clause: 120 (55,36) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x).

new given clause: 122 (66,44) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).

new given clause: 126 (79,44) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x).

------------ END OF SEARCH ------------

sos empty.

--------------- options ---------------
set(binary_res).
set(hyper_res).
set(UR_res).
set(demod_hist).
set(for_sub).
set(print_kept).
set(back_sub).
set(print_back_sub).
set(print_given).
set(check_arity).

clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
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                 22
clauses given                 94
clauses generated            846
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            6
clauses forward subsumed     724
(clauses subsumed by sos)    515
unit deletions                 0
clauses kept                 116
empty clauses                  0
factors generated              0
clauses back subsumed         33
clauses not processed          0

----------- times (seconds) -----------
run time            13.53
input time           0.24
binary_res time      1.05
hyper_res time       0.07
UR_res time          0.23
para_into time       0.00
para_from time       0.00
pre_process time     9.73
  demod time         0.00
  weigh time         0.04
  for_sub time       7.80
  unit_del time      0.00
post_process time    1.37
  back_sub time      1.07
  conflict time      0.01
  factor time        0.00
FPA build time       0.33
IS build time        0.14
print_cl time        0.98
cl integrate time    0.08
window time          0.00
SHAR_EOF
if test -f 'pigs.desc'
then
	echo shar: over-writing existing file "'pigs.desc'"
fi
cat << \SHAR_EOF > 'pigs.desc'
 problem-set/puzzles/carroll/pigs.desc
 created : 07/19/88
 revised : 07/19/88 

 description:
 This run solves "The Pigs and Balloons Puzzle" by Lewis Carroll
 using UR-resolution. 

		 The Pigs and Balloons Puzzle

 (1) All, who neither dance on tight ropes nor eat penny-buns,
     are old.
 (2) Pigs, that are liable to giddiness, are treated with respect.
 (3) A wise balloonist takes an umbrella with him.
 (4) No one ought to lunch in public who looks ridiculous and eats
     penny-buns.
 (5) Young creatures, who go up in balloons, are liable to 
     giddiness.
 (6) Fat creatures, who look ridiculous, may lunch in
     public, provided that they do not dance on tight ropes.
 (7) No wise creatures dance on tight ropes, if liable to giddiness.
 (8) A pig looks ridiculous, carrying an umbrella.
 (9) All, who do not dance on tight ropes, and who are treated
     with respect are fat.
     Show that no wise young pigs go up in balloons.
					-Lewis Carroll, Symbolic Logic, p. 378

Versions : 

pigs.ver1.in : Uses hyper-resolution, UR-resolution, and 
	binary-resolution.

		created by : Kelly Ratliff
		verified for ITP : unverified
		translated for OTTER by : K.R.
		verified for OTTER : 07/19/88
SHAR_EOF
if test -f 'pigs.ver1.clauses'
then
	echo shar: over-writing existing file "'pigs.ver1.clauses'"
fi
cat << \SHAR_EOF > 'pigs.ver1.clauses'
% problem-set/puzzles/carroll/pigs.ver1.clauses 
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Pigs and Balloons Puzzle" by Lewis Carroll
% using UR-resolution. 
%
%				 The Pigs and Balloons Puzzle
%
% (1) All, who neither dance on tight ropes nor eat penny-buns,
%     are old.
% (2) Pigs, that are liable to giddiness, are treated with respect.
% (3) A wise balloonist takes an umbrella with him.
% (4) No one ought to lunch in public who looks ridiculous and eats
%     penny-buns.
% (5) Young creatures, who go up in balloons, are liable to 
%     giddiness.
% (6) Fat creatures, who look ridiculous, may lunch in
%     public, provided that they do not dance on tight ropes.
% (7) No wise creatures dance on tight ropes, if liable to giddiness.
% (8) A pig looks ridiculous, carrying an umbrella.
% (9) All, who do not dance on tight ropes, and who are treated
%     with respect are fat.
%     Show that no wise young pigs go up in balloons.
%							-Lewis Carroll, Symbolic Logic, p. 378

% representation:
%
                  

% problem in clause form.

Dances_on_tightropes(x) | Eats_pennybuns(x) | Old(x).
-Pig(x)|-Liable_to_giddiness(x) | Treated_with_respect(x).
-Wise(x) | -Balloonist(x) | Has_umbrella(x).
-Looks_ridiculous(x) | -Eats_pennybuns(x) | -Eats_lunch_in_public(x).
-Balloonist(x) | -Young(x) | Liable_to_giddiness(x).
-Fat(x) | -Looks_ridiculous(x) | Dances_on_tightropes(x) |
Eats_lunch_in_public(x).
-Liable_to_giddiness(x) | -Wise(x) | -Dances_on_tightropes(x).
-Pig(x) | -Has_umbrella(x) | Looks_ridiculous(x).
Dances_on_tightropes(x) | -Treated_with_respect(x) | Fat(x).

% Everyone is young or old.

Young(x) | Old(x).
-Young(x) | -Old(x).
Wise(PIGGY).
Young(PIGGY).
Pig(PIGGY).
Balloonist(PIGGY).
SHAR_EOF
if test -f 'pigs.ver1.in'
then
	echo shar: over-writing existing file "'pigs.ver1.in'"
fi
cat << \SHAR_EOF > 'pigs.ver1.in'
% problem-set/puzzles/carroll/pigs.ver1.in
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Pigs and Balloons Puzzle" by Lewis Carroll
% using UR-resolution. 
%
%				 The Pigs and Balloons Puzzle
%
% (1) All, who neither dance on tight ropes nor eat penny-buns,
%     are old.
% (2) Pigs, that are liable to giddiness, are treated with respect.
% (3) A wise balloonist takes an umbrella with him.
% (4) No one ought to lunch in public who looks ridiculous and eats
%     penny-buns.
% (5) Young creatures, who go up in balloons, are liable to 
%     giddiness.
% (6) Fat creatures, who look ridiculous, may lunch in
%     public, provided that they do not dance on tight ropes.
% (7) No wise creatures dance on tight ropes, if liable to giddiness.
% (8) A pig looks ridiculous, carrying an umbrella.
% (9) All, who do not dance on tight ropes, and who are treated
%     with respect are fat.
%     Show that no wise young pigs go up in balloons.
%							-Lewis Carroll, Symbolic Logic, p. 378

% representation:
%

set(hyper_res).


list(axioms).

% problem in clause form.

Dances_on_tightropes(x) | Eats_pennybuns(x) | Old(x).
-Pig(x)|-Liable_to_giddiness(x) | Treated_with_respect(x).
-Wise(x) | -Balloonist(x) | Has_umbrella(x).
-Looks_ridiculous(x) | -Eats_pennybuns(x) | -Eats_lunch_in_public(x).
-Balloonist(x) | -Young(x) | Liable_to_giddiness(x).
-Fat(x) | -Looks_ridiculous(x) | Dances_on_tightropes(x) |
Eats_lunch_in_public(x).
-Liable_to_giddiness(x) | -Wise(x) | -Dances_on_tightropes(x).
-Pig(x) | -Has_umbrella(x) | Looks_ridiculous(x).
Dances_on_tightropes(x) | -Treated_with_respect(x) | Fat(x).

% Everyone is young or old.

Young(x) | Old(x).
-Young(x) | -Old(x).

end_of_list.


list(sos).

Wise(PIGGY).
Young(PIGGY).
Pig(PIGGY).
Balloonist(PIGGY).

end_of_list.
SHAR_EOF
if test -f 'pigs.ver1.out'
then
	echo shar: over-writing existing file "'pigs.ver1.out'"
fi
cat << \SHAR_EOF > 'pigs.ver1.out'
problem-set/puzzles/carroll/pigs.ver1.out
created : 07/19/88
revised : 07/19/88

OTTER version 0.91, 14 June 1988.

set(hyper_res).

list(axioms).
1 Dances_on_tightropes(x) | Eats_pennybuns(x) | Old(x).
2 -Pig(x) | -Liable_to_giddiness(x) | Treated_with_respect(x).
3 -Wise(x) | -Balloonist(x) | Has_umbrella(x).
4 -Looks_ridiculous(x) | -Eats_pennybuns(x) | -Eats_lunch_in_public(x).
5 -Balloonist(x) | -Young(x) | Liable_to_giddiness(x).
6 -Fat(x) | -Looks_ridiculous(x) | Dances_on_tightropes(x) | Eats_lunch_in_public(x).
7 -Liable_to_giddiness(x) | -Wise(x) | -Dances_on_tightropes(x).
8 -Pig(x) | -Has_umbrella(x) | Looks_ridiculous(x).
9 Dances_on_tightropes(x) | -Treated_with_respect(x) | Fat(x).
10 Young(x) | Old(x).
11 -Young(x) | -Old(x).
end_of_list.

list(sos).
12 Wise(PIGGY).
13 Young(PIGGY).
14 Pig(PIGGY).
15 Balloonist(PIGGY).
end_of_list.

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

1 Dances_on_tightropes(x) | Eats_pennybuns(x) | Old(x).
2 -Pig(x) | -Liable_to_giddiness(x) | Treated_with_respect(x).
3 -Wise(x) | -Balloonist(x) | Has_umbrella(x).
4 -Looks_ridiculous(x) | -Eats_pennybuns(x) | -Eats_lunch_in_public(x).
5 -Balloonist(x) | -Young(x) | Liable_to_giddiness(x).
6 -Fat(x) | -Looks_ridiculous(x) | Dances_on_tightropes(x) | Eats_lunch_in_public(x).
7 -Liable_to_giddiness(x) | -Wise(x) | -Dances_on_tightropes(x).
8 -Pig(x) | -Has_umbrella(x) | Looks_ridiculous(x).
9 Dances_on_tightropes(x) | -Treated_with_respect(x) | Fat(x).
11 -Young(x) | -Old(x).
12 Wise(PIGGY).
13 Young(PIGGY).
14 Pig(PIGGY).
15 Balloonist(PIGGY).
16 (13,11,1) Dances_on_tightropes(PIGGY) | Eats_pennybuns(PIGGY).
17 (15,5,13) Liable_to_giddiness(PIGGY).
18 (15,3,12) Has_umbrella(PIGGY).
20 (17,2,14) Treated_with_respect(PIGGY).
21 (18,8,14) Looks_ridiculous(PIGGY).
22 (20,9) Dances_on_tightropes(PIGGY) | Fat(PIGGY).
23 (16,7,17,12) Eats_pennybuns(PIGGY).
25 (22,6,21) Dances_on_tightropes(PIGGY) | Eats_lunch_in_public(PIGGY).
26 (25,7,17,12) Eats_lunch_in_public(PIGGY).
28 (26,4,21,23) .

--------------- options ---------------
set(hyper_res).
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(UR_res).
clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
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                 15
clauses given                 14
clauses generated             18
demodulation rewrites          0
clauses wt or lit delete       0
tautologies deleted            0
clauses forward subsumed       5
(clauses subsumed by sos)      4
unit deletions                 0
clauses kept                  13
empty clauses                  1
factors generated              0
clauses back subsumed          4
clauses not processed          1

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

 description:
 This run solves "The Winds and the Windows Puzzle" by Lewis Carroll
 using UR-resolution. 

                   The Winds and the Windows

 (1)  There is always sunshine when the wind is in the East.
 (2)  When it is cold and foggy, my neighbor practices the flute.
 (3)  When my fire smokes, I set the door open.
 (4)  When it is cold and I feel rheumatic, I light my fire.
 (5)  When the wind is in the East and comes in gusts, my fire smokes.
 (6)  When I keep the door open, I am free from headache.
 (7)  Even when the sun is shining and it is not cold, I keep my window
      shut if it is foggy.
 (8)  When the wind does not come in gusts, and when I have a fire
      and keep the door shut, I do not feel rheumatic.
 (9)  Sunshine always brings on fog.
 (10) When my neighbor practices the flute, I shut the door, even
      if I have no headache.
 (11) When there is a fog and the wind is in the East, I feel rheumatic
      Show that when the wind is in the East, I keep my windows shut.
					-Lewis Carroll, Symbolic Logic, p. 382

Versions : 

winds.ver1.in : Uses hyper-resolution

		created by : Kelly Ratliff
		verified for ITP : unverified
		translated for OTTER by : K.R.
		verified for OTTER : 07/19/88
SHAR_EOF
if test -f 'winds.ver1.clauses'
then
	echo shar: over-writing existing file "'winds.ver1.clauses'"
fi
cat << \SHAR_EOF > 'winds.ver1.clauses'
% problem-set/puzzles/carroll/winds.ver1.clauses 
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Winds and the Windows Puzzle" by Lewis Carroll
% using UR-resolution. 
%
%                   The Winds and the Windows
%
% (1)  There is always sunshine when the wind is in the East.
% (2)  When it is cold and foggy, my neighbor practices the flute.
% (3)  When my fire smokes, I set the door open.
% (4)  When it is cold and I feel rheumatic, I light my fire.
% (5)  When the wind is in the East and comes in gusts, my fire smokes.
% (6)  When I keep the door open, I am free from headache.
% (7)  Even when the sun is shining and it is not cold, I keep my window
%      shut if it is foggy.
% (8)  When the wind does not come in gusts, and when I have a fire
%      and keep the door shut, I do not feel rheumatic.
% (9)  Sunshine always brings on fog.
% (10) When my neighbor practices the flute, I shut the door, even
%      if I have no headache.
% (11) When there is a fog and the wind is in the East, I feel rheumatic
%      Show that when the wind is in the East, I keep my windows shut.
%							-Lewis Carroll, Symbolic Logic, p. 382

% representation:
%
                  
-WIND_IN_EAST | SUNSHINE.
-COLD | -FOGGY | NEIGHBOR_PRACTICES_FLUTE.
-FIRE_SMOKES | DOOR_IS_OPEN.
-COLD | -I_FEEL_RHEUMATIC | FIRE_IS_LIT.
-WIND_IN_EAST | -WIND_IN_GUSTS | FIRE_SMOKES.
-DOOR_IS_OPEN | -HEADACHE.
-SUNSHINE | COLD | -FOGGY | WINDOW_IS_SHUT.
WIND_IN_GUSTS | -FIRE_IS_LIT | DOOR_IS_OPEN | -I_FEEL_RHEUMATIC.
-SUNSHINE | FOGGY.
-NEIGHBOR_PRACTICES_FLUTE | -DOOR_IS_OPEN.
-FOGGY | -WIND_IN_EAST | I_FEEL_RHEUMATIC.
WIND_IN_EAST.
-WINDOW_IS_SHUT.
SHAR_EOF
if test -f 'winds.ver1.in'
then
	echo shar: over-writing existing file "'winds.ver1.in'"
fi
cat << \SHAR_EOF > 'winds.ver1.in'
% problem-set/puzzles/carroll/winds.ver1.in
% created : 07/19/88
% revised : 07/19/88 

% description:
%
% This run solves "The Winds and the Windows Puzzle" by Lewis Carroll
% using UR-resolution. 
%
%                   The Winds and the Windows
%
% (1)  There is always sunshine when the wind is in the East.
% (2)  When it is cold and foggy, my neighbor practices the flute.
% (3)  When my fire smokes, I set the door open.
% (4)  When it is cold and I feel rheumatic, I light my fire.
% (5)  When the wind is in the East and comes in gusts, my fire smokes.
% (6)  When I keep the door open, I am free from headache.
% (7)  Even when the sun is shining and it is not cold, I keep my window
%      shut if it is foggy.
% (8)  When the wind does not come in gusts, and when I have a fire
%      and keep the door shut, I do not feel rheumatic.
% (9)  Sunshine always brings on fog.
% (10) When my neighbor practices the flute, I shut the door, even
%      if I have no headache.
% (11) When there is a fog and the wind is in the East, I feel rheumatic
%      Show that when the wind is in the East, I keep my windows shut.
%							-Lewis Carroll, Symbolic Logic, p. 382

% representation:
%
                  
set(hyper_res).


list(axioms).

-WIND_IN_EAST | SUNSHINE.
-COLD | -FOGGY | NEIGHBOR_PRACTICES_FLUTE.
-FIRE_SMOKES | DOOR_IS_OPEN.
-COLD | -I_FEEL_RHEUMATIC | FIRE_IS_LIT.
-WIND_IN_EAST | -WIND_IN_GUSTS | FIRE_SMOKES.
-DOOR_IS_OPEN | -HEADACHE.
-SUNSHINE | COLD | -FOGGY | WINDOW_IS_SHUT.
WIND_IN_GUSTS | -FIRE_IS_LIT | DOOR_IS_OPEN | -I_FEEL_RHEUMATIC.
-SUNSHINE | FOGGY.
-NEIGHBOR_PRACTICES_FLUTE | -DOOR_IS_OPEN.
-FOGGY | -WIND_IN_EAST | I_FEEL_RHEUMATIC.

end_of_list.


list(sos).

WIND_IN_EAST.
-WINDOW_IS_SHUT.

end_of_list.
SHAR_EOF
if test -f 'winds.ver1.out'
then
	echo shar: over-writing existing file "'winds.ver1.out'"
fi
cat << \SHAR_EOF > 'winds.ver1.out'
problem-set/puzzles/carroll/winds.ver1.out
created : 07/19/88
revised : 07/19/88

OTTER version 0.91, 14 June 1988.

set(hyper_res).

list(axioms).
1 -WIND_IN_EAST | SUNSHINE.
2 -COLD | -FOGGY | NEIGHBOR_PRACTICES_FLUTE.
3 -FIRE_SMOKES | DOOR_IS_OPEN.
4 -COLD | -I_FEEL_RHEUMATIC | FIRE_IS_LIT.
5 -WIND_IN_EAST | -WIND_IN_GUSTS | FIRE_SMOKES.
6 -DOOR_IS_OPEN | -HEADACHE.
7 -SUNSHINE | COLD | -FOGGY | WINDOW_IS_SHUT.
8 WIND_IN_GUSTS | -FIRE_IS_LIT | DOOR_IS_OPEN | -I_FEEL_RHEUMATIC.
9 -SUNSHINE | FOGGY.
10 -NEIGHBOR_PRACTICES_FLUTE | -DOOR_IS_OPEN.
11 -FOGGY | -WIND_IN_EAST | I_FEEL_RHEUMATIC.
end_of_list.

list(sos).
12 WIND_IN_EAST.
13 -WINDOW_IS_SHUT.
end_of_list.

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

1 -WIND_IN_EAST | SUNSHINE.
2 -COLD | -FOGGY | NEIGHBOR_PRACTICES_FLUTE.
3 -FIRE_SMOKES | DOOR_IS_OPEN.
4 -COLD | -I_FEEL_RHEUMATIC | FIRE_IS_LIT.
5 -WIND_IN_EAST | -WIND_IN_GUSTS | FIRE_SMOKES.
7 -SUNSHINE | COLD | -FOGGY | WINDOW_IS_SHUT.
8 WIND_IN_GUSTS | -FIRE_IS_LIT | DOOR_IS_OPEN | -I_FEEL_RHEUMATIC.
9 -SUNSHINE | FOGGY.
10 -NEIGHBOR_PRACTICES_FLUTE | -DOOR_IS_OPEN.
11 -FOGGY | -WIND_IN_EAST | I_FEEL_RHEUMATIC.
12 WIND_IN_EAST.
13 -WINDOW_IS_SHUT.
14 (12,1) SUNSHINE.
15 (14,9) FOGGY.
16 (15,11,12) I_FEEL_RHEUMATIC.
17 (15,7,14) COLD | WINDOW_IS_SHUT.
20 (17,13) COLD.
21 (20,4,16) FIRE_IS_LIT.
22 (20,2,15) NEIGHBOR_PRACTICES_FLUTE.
23 (21,8,16) WIND_IN_GUSTS | DOOR_IS_OPEN.
25 (23,10,22) WIND_IN_GUSTS.
26 (25,5,12) FIRE_SMOKES.
27 (26,3) DOOR_IS_OPEN.
28 (27,10,22) .

--------------- options ---------------
set(hyper_res).
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(UR_res).
clear(para_from).
clear(para_into).
clear(demod_inf).
clear(para_from_left).
clear(para_from_right).
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                 13
clauses given                 13
clauses generated             15
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                  15
empty clauses                  1
factors generated              0
clauses back subsumed         14
clauses not processed          0

----------- times (seconds) -----------
run time             0.40
input time           0.11
binary_res time      0.00
hyper_res time       0.03
UR_res time          0.00
para_into time       0.00
para_from time       0.00
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.06
  back_sub time      0.01
  conflict time      0.00
  factor time        0.00
FPA build time       0.02
IS build time        0.01
print_cl time        0.11
cl integrate time    0.00
window time          0.00
SHAR_EOF
#	End of shell archive
exit 0