#!/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