#!/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 # barber.desc # barber.ver1.clauses # barber.ver1.in # barber.ver1.out # boxes.desc # boxes.ver1.clauses # boxes.ver1.in # boxes.ver1.out # houses.desc # houses.ver1.clauses # houses.ver1.in # houses.ver1.out # jobs.desc # jobs.ver1.clauses # jobs.ver1.in # jobs.ver1.out # steamroller.desc # steamroller.ver1.clauses # steamroller.ver1.in # steamroller.ver1.out # steamroller.ver2.clauses # steamroller.ver2.in # steamroller.ver2.out # This archive created: Tue Aug 16 11:23:26 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/miscell/README created : 07/26/88 revised : 07/26/88 Contents of 'miscell' : ----------------------- Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/puzzles/miscell. barber : to solve "The Barber Puzzle" boxes : to solve "The Mislabeled Boxes" houses : to solve "The Houses Puzzle" jobs : to solve "The Jobs Puzzle" steamroller : to solve "Schubert's Steamroller Puzzle" ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a % and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in through OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background. SHAR_EOF if test -f 'barber.desc' then echo shar: over-writing existing file "'barber.desc'" fi cat << \SHAR_EOF > 'barber.desc' problem-set/puzzles/miscell/barber.desc created : 07/05/88 revised : 07/05/88 Natural Language Description: The Barber Puzzle There is a barbers' club that obeys the following three conditions: (1) If any member has shaved any other member -- whether himself or another -- then all members have shaved him, though not necess- arily at the same time. (2) Four of the members are named Guido, Lorenzo, Petrucio, and Cesare. (3) Guido has shaved Cesare. Has Petrucio shaved Lorenzo or not? Versions: barber.ver1.in- Non-procedural representation. created by : ?. verified for ITP : 07/05/88 translated for OTTER by : K.R. verified for OTTER : 07/05/88 SHAR_EOF if test -f 'barber.ver1.clauses' then echo shar: over-writing existing file "'barber.ver1.clauses'" fi cat << \SHAR_EOF > 'barber.ver1.clauses' % problem-set/puzzles/miscell/barber.ver1.clauses % created : 07/05/88 % revised : 07/05/88 % description: % % This run solves "The Barber Puzzle" using UR-resolution. % % The Barber Puzzle % % There is a barbers' club that obeys the following three conditions: % (1) If any member has shaved any other member -- whether himself or % another -- then all members have shaved him, though not necess- % arily at the same time. % (2) Four of the members are named Guido, Lorenzo, Petrucio, and % Cesare. % (3) Guido has shaved Cesare. % Has Petrucio shaved Lorenzo or not? % representation: % % Non-procedural version % PREDICATES: MEMBER(x) : x is a member of the barbers club . % SHAVED(x,y) : x has shaved y . -MEMBER(x) |-MEMBER(y) | -SHAVED(x,y) | SHAVED(members,x). -SHAVED(members,x) | -MEMBER(y) | SHAVED(y,x). -SHAVED(Petruchio,Lorenzo) | ANSWER(Yes) . MEMBER(Guido). MEMBER(Lorenzo). MEMBER(Petruchio). MEMBER(Cesare). SHAVED(Guido,Cesare). SHAR_EOF if test -f 'barber.ver1.in' then echo shar: over-writing existing file "'barber.ver1.in'" fi cat << \SHAR_EOF > 'barber.ver1.in' % problem-set/puzzles/miscell/barber.ver1.in % created : % revised : 07/05/88 % description: % % This run solves "The Barber Puzzle" using UR-resolution. % % The Barber Puzzle % % There is a barbers' club that obeys the following three conditions: % (1) If any member has shaved any other member -- whether himself or % another -- then all members have shaved him, though not necess- % arily at the same time. % (2) Four of the members are named Guido, Lorenzo, Petrucio, and % Cesare. % (3) Guido has shaved Cesare. % Has Petrucio shaved Lorenzo or not? % representation: % % Non-procedural version % PREDICATES: MEMBER(x) : x is a member of the barbers club . % SHAVED(x,y) : x has shaved y . set(UR_res). list(axioms). -MEMBER(x) |-MEMBER(y) | -SHAVED(x,y) | SHAVED(members,x). -SHAVED(members,x) | -MEMBER(y) | SHAVED(y,x). -SHAVED(Petruchio,Lorenzo) | ANSWER(Yes) . end_of_list. list(sos). MEMBER(Guido). MEMBER(Lorenzo). MEMBER(Petruchio). MEMBER(Cesare). SHAVED(Guido,Cesare). end_of_list. SHAR_EOF if test -f 'barber.ver1.out' then echo shar: over-writing existing file "'barber.ver1.out'" fi cat << \SHAR_EOF > 'barber.ver1.out' problem-set/puzzles/miscell/barber.ver1.out created : 07/05/88 revised : 07/15/88 OTTER release 0.9, 19 May 1988 set(UR_res). list(axioms). 1 -MEMBER(x) | -MEMBER(y) | -SHAVED(x,y) | SHAVED(members,x). 2 -SHAVED(members,x) | -MEMBER(y) | SHAVED(y,x). 3 -SHAVED(Petruchio,Lorenzo) | ANSWER(Yes). end_of_list. list(sos). 4 MEMBER(Guido). 5 MEMBER(Lorenzo). 6 MEMBER(Petruchio). 7 MEMBER(Cesare). 8 SHAVED(Guido,Cesare). end_of_list. new given clause: 4 MEMBER(Guido). new given clause: 5 MEMBER(Lorenzo). new given clause: 6 MEMBER(Petruchio). new given clause: 7 MEMBER(Cesare). new given clause: 8 SHAVED(Guido,Cesare). ** KEPT: 9 (8,1,4,7) SHAVED(members,Guido). new given clause: 9 (8,1,4,7) SHAVED(members,Guido). ** KEPT: 10 (9,2,7) SHAVED(Cesare,Guido). ** KEPT: 11 (9,2,6) SHAVED(Petruchio,Guido). ** KEPT: 12 (9,2,5) SHAVED(Lorenzo,Guido). ** KEPT: 13 (9,2,4) SHAVED(Guido,Guido). new given clause: 10 (9,2,7) SHAVED(Cesare,Guido). ** KEPT: 14 (10,1,7,4) SHAVED(members,Cesare). new given clause: 11 (9,2,6) SHAVED(Petruchio,Guido). ** KEPT: 15 (11,1,6,4) SHAVED(members,Petruchio). new given clause: 12 (9,2,5) SHAVED(Lorenzo,Guido). ** KEPT: 16 (12,1,5,4) SHAVED(members,Lorenzo). new given clause: 13 (9,2,4) SHAVED(Guido,Guido). new given clause: 14 (10,1,7,4) SHAVED(members,Cesare). ** KEPT: 17 (14,2,7) SHAVED(Cesare,Cesare). ** KEPT: 18 (14,2,6) SHAVED(Petruchio,Cesare). ** KEPT: 19 (14,2,5) SHAVED(Lorenzo,Cesare). new given clause: 15 (11,1,6,4) SHAVED(members,Petruchio). ** KEPT: 20 (15,2,7) SHAVED(Cesare,Petruchio). ** KEPT: 21 (15,2,6) SHAVED(Petruchio,Petruchio). ** KEPT: 22 (15,2,5) SHAVED(Lorenzo,Petruchio). ** KEPT: 23 (15,2,4) SHAVED(Guido,Petruchio). new given clause: 16 (12,1,5,4) SHAVED(members,Lorenzo). ** KEPT: 24 (16,2,7) SHAVED(Cesare,Lorenzo). ** KEPT: 25 (16,2,6) SHAVED(Petruchio,Lorenzo). ** KEPT: 26 (16,2,5) SHAVED(Lorenzo,Lorenzo). ** KEPT: 27 (16,2,4) SHAVED(Guido,Lorenzo). new given clause: 17 (14,2,7) SHAVED(Cesare,Cesare). new given clause: 18 (14,2,6) SHAVED(Petruchio,Cesare). new given clause: 19 (14,2,5) SHAVED(Lorenzo,Cesare). new given clause: 20 (15,2,7) SHAVED(Cesare,Petruchio). new given clause: 21 (15,2,6) SHAVED(Petruchio,Petruchio). new given clause: 22 (15,2,5) SHAVED(Lorenzo,Petruchio). new given clause: 23 (15,2,4) SHAVED(Guido,Petruchio). new given clause: 24 (16,2,7) SHAVED(Cesare,Lorenzo). new given clause: 25 (16,2,6) SHAVED(Petruchio,Lorenzo). ** KEPT: 28 (25,3) ANSWER(Yes). 28 back subsumes: 3 -SHAVED(Petruchio,Lorenzo) | ANSWER(Yes). new given clause: 28 (25,3) ANSWER(Yes). new given clause: 26 (16,2,5) SHAVED(Lorenzo,Lorenzo). new given clause: 27 (16,2,4) SHAVED(Guido,Lorenzo). ------------ END OF SEARCH ------------ sos empty. --------------- 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 8 clauses given 25 clauses generated 33 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 13 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 20 empty clauses 0 factors generated 0 clauses back subsumed 1 clauses not processed 0 ----------- times (seconds) ----------- run time 0.64 input time 0.08 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.24 para_into time 0.00 para_from time 0.00 pre_process time 0.11 demod time 0.00 weigh time 0.00 for_sub time 0.02 unit_del time 0.00 post_process time 0.05 back_sub time 0.02 conflict time 0.02 factor time 0.00 FPA build time 0.03 IS build time 0.01 print_cl time 0.09 cl integrate time 0.01 window time 0.00 SHAR_EOF if test -f 'boxes.desc' then echo shar: over-writing existing file "'boxes.desc'" fi cat << \SHAR_EOF > 'boxes.desc' problem-set/puzzles/miscell/boxes.desc created : 07/09/86 revised : 07/14/88 Natural Language Description: The Mislabeled Boxes There are three boxes a, b, and c on a table. Each box contains apples or bananas or oranges. No two boxes contain the same thing. Each box has a label that says it contains apples or says it contains bananas or says it contains oranges. No box contains what it says on its label. The label on box a says "apples". The label on box b says "oranges". The label on box c says "bananas". You pick up box b and it contains apples. What do the other two boxes contain? Versions: boxes.ver1.in : declarative representation. answer: box a contains bananas and box c contains oranges. created by : W. McCune. verified for ITP : 07/05/88 translated for OTTER by : K.R. verified for OTTER : 07/05/88 SHAR_EOF if test -f 'boxes.ver1.clauses' then echo shar: over-writing existing file "'boxes.ver1.clauses'" fi cat << \SHAR_EOF > 'boxes.ver1.clauses' % problem-set/puzzles/miscell/boxes.ver1.clauses % created : 07/14/88 % revised : 07/14/88 % description: % % This run solves a puzzle called "The Mislabeled Boxes" using % UR-resolution. % % The Mislabeled Boxes % % There are three boxes a, b, and c on a table. % Each box contains apples or bananas or oranges. % No two boxes contain the same thing. % Each box has a label that says it contains apples % or says it contains bananas or says it contains % oranges. % No box contains what it says on its label. % The label on box a says "apples". % The label on box b says "oranges". % The label on box c says "bananas". % You pick up box b and it contains apples. % What do the other two boxes contain? % representation: % % declare_predicates(2,[EQB,EQF,LABEL,CONTAINS]). % declare_variables([x,y,z]). % declare_constants([boxa,boxb,boxc,ap,or,ban]). % % Declarative version % PREDICATES: % EQB = Same boxe; EQF = Same fruit. % LABEL(x,y) = The label on box 'x' is 'y'. % CONTAINS(x,y) = The contents of box 'x' is 'y'. % boxa,boxb,boxc = The different box #s a,b,c. % ap = apples; or = oranges; ban = bananas. % Equality axioms . EQF(x,x). EQB(x,x). % The boxes are mislabelled . -LABEL(x,y) | -CONTAINS(x,y). % Each box has at least one fruit, and each fruit is in at least one box CONTAINS(boxa,x) | CONTAINS(boxb,x) | CONTAINS(boxc,x). CONTAINS(x,ap) | CONTAINS(x,ban) | CONTAINS(x,or). % A box has at most one fruit, and a fruit is in at most one box. -CONTAINS(x,y) | -CONTAINS(x,z) | EQF(y,z). -CONTAINS(x,y) | -CONTAINS(z,y) | EQB(x,z). % The boxes are unique . -EQB(boxa,boxb). -EQB(boxb,boxc). -EQB(boxa,boxc). % The fruits are unique . -EQF(ap,ban). -EQF(ban,or). -EQF(ap,or). % Given clauses . LABEL(boxa,ap). LABEL(boxb,or). LABEL(boxc,ban). CONTAINS(boxb,ap). SHAR_EOF if test -f 'boxes.ver1.in' then echo shar: over-writing existing file "'boxes.ver1.in'" fi cat << \SHAR_EOF > 'boxes.ver1.in' % problem-set/puzzles/miscell/boxes.ver1.in % created : 07/09/86 % revised : 07/05/88 % description: % % This run solves a puzzle called "The Mislabeled Boxes" using % UR-resolution. % % The Mislabeled Boxes % % There are three boxes a, b, and c on a table. % Each box contains apples or bananas or oranges. % No two boxes contain the same thing. % Each box has a label that says it contains apples % or says it contains bananas or says it contains % oranges. % No box contains what it says on its label. % The label on box a says "apples". % The label on box b says "oranges". % The label on box c says "bananas". % You pick up box b and it contains apples. % What do the other two boxes contain? % representation: % % declare_predicates(2,[EQB,EQF,LABEL,CONTAINS]). % declare_variables([x,y,z]). % declare_constants([boxa,boxb,boxc,ap,or,ban]). % % Declarative version % PREDICATES: % EQB = Same boxe; EQF = Same fruit. % LABEL(x,y) = The label on box 'x' is 'y'. % CONTAINS(x,y) = The contents of box 'x' is 'y'. % boxa,boxb,boxc = The different box #s a,b,c. % ap = apples; or = oranges; ban = bananas. set(UR_res). list(axioms). % Equality axioms . EQF(x,x). EQB(x,x). % The boxes are mislabelled . -LABEL(x,y) | -CONTAINS(x,y). % Each box has at least one fruit, and each fruit is in at least one box CONTAINS(boxa,x) | CONTAINS(boxb,x) | CONTAINS(boxc,x). CONTAINS(x,ap) | CONTAINS(x,ban) | CONTAINS(x,or). % A box has at most one fruit, and a fruit is in at most one box. -CONTAINS(x,y) | -CONTAINS(x,z) | EQF(y,z). -CONTAINS(x,y) | -CONTAINS(z,y) | EQB(x,z). % The boxes are unique . -EQB(boxa,boxb). -EQB(boxb,boxc). -EQB(boxa,boxc). % The fruits are unique . -EQF(ap,ban). -EQF(ban,or). -EQF(ap,or). end_of_list. list(sos). % Given clauses . LABEL(boxa,ap). LABEL(boxb,or). LABEL(boxc,ban). CONTAINS(boxb,ap). end_of_list. SHAR_EOF if test -f 'boxes.ver1.out' then echo shar: over-writing existing file "'boxes.ver1.out'" fi cat << \SHAR_EOF > 'boxes.ver1.out' problem-set/puzzles/miscell/boxes.ver1.out created : 07/14/88 revised : 07/14/88 OTTER release 0.9, 19 May 1988 set(UR_res). list(axioms). 1 EQF(x,x). 2 EQB(x,x). 3 -LABEL(x,y) | -CONTAINS(x,y). 4 CONTAINS(boxa,x) | CONTAINS(boxb,x) | CONTAINS(boxc,x). 5 CONTAINS(x,ap) | CONTAINS(x,ban) | CONTAINS(x,or). 6 -CONTAINS(x,y) | -CONTAINS(x,z) | EQF(y,z). 7 -CONTAINS(x,y) | -CONTAINS(z,y) | EQB(x,z). 8 -EQB(boxa,boxb). 9 -EQB(boxb,boxc). 10 -EQB(boxa,boxc). 11 -EQF(ap,ban). 12 -EQF(ban,or). 13 -EQF(ap,or). end_of_list. list(sos). 14 LABEL(boxa,ap). 15 LABEL(boxb,or). 16 LABEL(boxc,ban). 17 CONTAINS(boxb,ap). end_of_list. new given clause: 14 LABEL(boxa,ap). ** KEPT: 18 (14,3) -CONTAINS(boxa,ap). new given clause: 15 LABEL(boxb,or). ** KEPT: 19 (15,3) -CONTAINS(boxb,or). new given clause: 16 LABEL(boxc,ban). ** KEPT: 20 (16,3) -CONTAINS(boxc,ban). new given clause: 17 CONTAINS(boxb,ap). ** KEPT: 21 (17,7,9) -CONTAINS(boxc,ap). ** KEPT: 22 (17,6,11) -CONTAINS(boxb,ban). ** KEPT: 23 (17,3) -LABEL(boxb,ap). new given clause: 18 (14,3) -CONTAINS(boxa,ap). new given clause: 19 (15,3) -CONTAINS(boxb,or). new given clause: 20 (16,3) -CONTAINS(boxc,ban). new given clause: 21 (17,7,9) -CONTAINS(boxc,ap). ** KEPT: 24 (21,5,20) CONTAINS(boxc,or). new given clause: 22 (17,6,11) -CONTAINS(boxb,ban). ** KEPT: 25 (22,4,20) CONTAINS(boxa,ban). new given clause: 23 (17,3) -LABEL(boxb,ap). new given clause: 24 (21,5,20) CONTAINS(boxc,or). ** KEPT: 26 (24,7,10) -CONTAINS(boxa,or). ** KEPT: 27 (24,3) -LABEL(boxc,or). new given clause: 25 (22,4,20) CONTAINS(boxa,ban). ** KEPT: 28 (25,3) -LABEL(boxa,ban). new given clause: 26 (24,7,10) -CONTAINS(boxa,or). new given clause: 27 (24,3) -LABEL(boxc,or). new given clause: 28 (25,3) -LABEL(boxa,ban). ------------ END OF SEARCH ------------ sos empty. --------------- 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 17 clauses given 15 clauses generated 36 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 25 (clauses subsumed by sos) 3 unit deletions 0 clauses kept 11 empty clauses 0 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.54 input time 0.15 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.13 para_into time 0.00 para_from time 0.00 pre_process time 0.09 demod time 0.00 weigh time 0.00 for_sub time 0.04 unit_del time 0.00 post_process time 0.03 back_sub time 0.01 conflict time 0.02 factor time 0.00 FPA build time 0.03 IS build time 0.01 print_cl time 0.07 cl integrate time 0.01 window time 0.00 SHAR_EOF if test -f 'houses.desc' then echo shar: over-writing existing file "'houses.desc'" fi cat << \SHAR_EOF > 'houses.desc' problem-set/puzzles/miscell/houses.desc created : 08/02/88 revised : 08/11/88 Natural Language Description: The Houses There are 5 houses, 5 people, 5 colors, 5 drinks, 5 games, and 4 pets. Each house has a person, a color, a drink, and game, and all but one of the houses has a pet. The problem is to match each house with as many properties as possible. House 1 is at the left end and house 5 is at the right end. The Englishman lives in the Red house. The White house is left of the Green house. The Italian has a Guppy. Lemonade is drunk in the Green house. The Swede lives in the house where Coffee is drunk. The Toad lives in the house where Backgammon is played. Racquetball is played in the Yellow house. Milk is drunk in the third house. The Russian lives in the first house. The Camel lives next to the house where Quoits is played. The Rat lives next to the house where Racquetball is played. Solitaire is played in the house where Vodka is drunk. The American lives in the house where Charades is played. The Russian lives next to the Blue house. Versions: houses.ver1 : uses UR-resolution, binary-resolution, factoring, and Unit-deletion to obtain the units for the solution, and weighting to obtain the contradiction. created by : Kelly Ratliff verified for ITP : untested translated for OTTER : K.R. verified for OTTER : 08/11/88 SHAR_EOF if test -f 'houses.ver1.clauses' then echo shar: over-writing existing file "'houses.ver1.clauses'" fi cat << \SHAR_EOF > 'houses.ver1.clauses' % problem-set/puzzles/miscell/houses.ver1.clauses % created : 08/02/88 % revised : 08/11/88 % description: % % This run solves "The Houses" puzzle using binary-resolution % and UR-resolution, factoring, unit-deletion, and weighting. % % The Houses % % There are 5 houses, 5 people, 5 colors, 5 drinks, 5 games, % and 4 pets. Each house has a person, a color, a drink, and % game, and all but one of the houses has a pet. The problem % is to match each house with as many properties as possible. % House 1 is at the left end and house 5 is at the right end. % The Englishman lives in the Red house. The White house is % left of the Green house. The Italian has a Guppy. Lemonade % is drunk in the Green house. The Swede lives in the house % where Coffee is drunk. The Toad lives in the house where % Backgammon is played. Racquetball is played in the Yellow % house. Milk is drunk in the third house. The Russian lives % in the first house. The Camel lives next to the house where % Quoits is played. The Rat lives next to the house where % Racquetball is played. Solitaire is played in the house % where Vodka is drunk. The American lives in the house % where Charades is played. The Russian lives next to the Blue % house. % representation: % % Predicates: % samehouse, sameperson, samecolor, samedrink, samegame, and % samepet predicates indicate that both arguments are % identical items. % nextto(x,y) indicates that house x is immediately next to % house y. on either side. % left(x,y) indicates that house x is to the immediate left % of house y. % hasperson, hascolor, hasdrink, hasgame, haspet predicates % indicate that the house identified by the first argument % has the item indicated by the second argument. % definition of samehouse samehouse(x,x). -samehouse(1,2). -samehouse(1,3). -samehouse(1,4). -samehouse(1,5). -samehouse(2,3). -samehouse(2,4). -samehouse(2,5). -samehouse(3,4). -samehouse(3,5). -samehouse(4,5). % definition of sameperson sameperson(x,x). -sameperson(Englishman,Italian). -sameperson(Englishman,Swede). -sameperson(Englishman,Russian). -sameperson(Englishman,American). -sameperson(Italian,Swede). -sameperson(Italian,Russian). -sameperson(Italian,American). -sameperson(Swede,Russian). -sameperson(Swede,American). -sameperson(Russian,American). % definition of samecolor samecolor(x,x). -samecolor(Red,White). -samecolor(Red,Green). -samecolor(Red,Yellow). -samecolor(Red,Blue). -samecolor(White,Green). -samecolor(White,Yellow). -samecolor(White,Blue). -samecolor(Green,Yellow). -samecolor(Green,Blue). -samecolor(Yellow,Blue). % definition of samedrink samedrink(x,x). -samedrink(Lemonade,Coffee). -samedrink(Lemonade,Milk). -samedrink(Lemonade,Vodka). -samedrink(Lemonade,Unknowndrink). -samedrink(Coffee,Milk). -samedrink(Coffee,Vodka). -samedrink(Coffee,Unknowndrink). -samedrink(Milk,Vodka). -samedrink(Milk,Unknowndrink). -samedrink(Vodka,Unknowndrink). % definition of samegame samegame(x,x). -samegame(Backgammon,Racquetball). -samegame(Backgammon,Quoits). -samegame(Backgammon,Solitaire). -samegame(Backgammon,Charades). -samegame(Racquetball,Quoits). -samegame(Racquetball,Solitaire). -samegame(Racquetball,Charades). -samegame(Quoits,Solitaire). -samegame(Quoits,Charades). -samegame(Solitaire,Charades). % definition of samepet samepet(x,x). -samepet(Guppy,Toad). -samepet(Guppy,Camel). -samepet(Guppy,Rat). -samepet(Guppy,No_pet). -samepet(Toad,Camel). -samepet(Toad,Rat). -samepet(Toad,No_pet). -samepet(Camel,Rat). -samepet(Camel,No_pet). -samepet(Rat,No_pet). % Definition and properties of nextto and left -nextto(x,y) | nextto(y,x). -left(x,y) | -left(y,x). -nextto(x,y) | left(x,y) | left(y,x). -left(x,y) | nextto(x,y). -samehouse(x,y) | -nextto(x,y). -left(x,x). -nextto(x,x). % Each house has a person and each person has a house: hasperson(x,Englishman) | hasperson(x,Italian) | hasperson(x,Swede) | hasperson(x,Russian) | hasperson(x,American). hasperson(1,y) | hasperson(2,y) | hasperson(3,y) | hasperson(4,y) | hasperson(5,y). % Each house has a color and each color has a house: hascolor(x,Red) | hascolor(x,White) | hascolor(x,Green) | hascolor(x,Yellow) | hascolor(x,Blue). hascolor(1,y) | hascolor(2,y) | hascolor(3,y) | hascolor(4,y) | hascolor(5,y). % Each house has a drink and each drink has a house: hasdrink(x,Lemonade) | hasdrink(x,Coffee) | hasdrink(x,Milk) | hasdrink(x,Vodka) | hasdrink(x,Unknowndrink). hasdrink(1,y) | hasdrink(2,y) | hasdrink(3,y) | hasdrink(4,y) | hasdrink(5,y). % Each house has a game and each game has a house: hasgame(x,Backgammon) | hasgame(x,Racquetball) | hasgame(x,Quoits) | hasgame(x,Solitaire) | hasgame(x,Charades). hasgame(1,y) | hasgame(2,y) | hasgame(3,y) | hasgame(4,y) | hasgame(5,y). % Each house has a pet and each pet has a house: haspet(x,Guppy) | haspet(x,Toad) | haspet(x,Camel) | haspet(x,Rat) | haspet(x,No_pet). haspet(1,y) | haspet(2,y) | haspet(3,y) | haspet(4,y) | haspet(5,y). % Unique items to each house: samehouse(x1,x2) | -hascolor(x1,y) | -hascolor(x2,y). samehouse(x1,x2) | -hasperson(x1,y) | -hasperson(x2,y). samehouse(x1,x2) | -hasdrink(x1,y) | -hasdrink(x2,y). samehouse(x1,x2) | -hasgame(x1,y) | -hasgame(x2,y). samehouse(x1,x2) | -haspet(x1,y) | -haspet(x2,y). sameperson(x1,x2) | -hasperson(y,x1) | -hasperson(y,x2). samecolor(x1,x2) | -hascolor(y,x1) | -hascolor(y,x2). samedrink(x1,x2) | -hasdrink(y,x1) | -hasdrink(y,x2). samegame(x1,x2) | -hasgame(y,x1) | -hasgame(y,x2). samepet(x1,x2) | -haspet(y,x1) | -haspet(y,x2). % The Englishman lives in the Red house -hasperson(x,Englishman) | hascolor(x,Red). hasperson(x,Englishman) | -hascolor(x,Red). % The White house is left of the Green house. -hascolor(x,White) | -hascolor(y,Green) | left(x,y). -hascolor(x,White) | hascolor(y,Green) | -left(x,y). hascolor(x,White) | -hascolor(y,Green) | -left(x,y). % The Italian has a Guppy. -hasperson(x,Italian) | haspet(x,Guppy). hasperson(x,Italian) | -haspet(x,Guppy). % Lemonade is drunk is the Green house. -hasdrink(x,Lemonade) | hascolor(x,Green). hasdrink(x,Lemonade) | -hascolor(x,Green). % The Swede lives in the house where Coffee is drunk. -hasperson(x,Swede) | hasdrink(x,Coffee). hasperson(x,Swede) | -hasdrink(x,Coffee). % The Toad lives in the house where Backgammon is played. -haspet(x,Toad) | hasgame(x,Backgammon). haspet(x,Toad) | -hasgame(x,Backgammon). % Racquetball is played in the Yellow house. -hasgame(x,Racquetball) | hascolor(x,Yellow). hasgame(x,Racquetball) | -hascolor(x,Yellow). % The Camel lives next to the house where Quoits is played. -haspet(x,Camel) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hasgame(y,Quoits) | hasgame(z,Quoits). -haspet(x,Camel) | -samehouse(1,x) | -nextto(x,y) | hasgame(y,Quoits). -haspet(x,Camel) | -samehouse(x,5) | -nextto(x,y) | hasgame(y,Quoits). -haspet(x,Camel) | nextto(x,y) | -hasgame(y,Quoits). samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Quoits) | haspet(y,Camel) | haspet(z,Camel). -samehouse(1,x) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel). -samehouse(x,5) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel). % The Rat lives next to the house where Racquetball is played. -haspet(x,Rat) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hasgame(y,Racquetball) | hasgame(z,Racquetball). -haspet(x,Rat) | -nextto(x,y) | -samehouse(1,x) | hasgame(y,Racquetball). -haspet(x,Rat) | -nextto(x,y) | -samehouse(x,5) | hasgame(y,Racquetball). -haspet(x,Rat) | nextto(x,y) | -hasgame(y,Racquetball). samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Racquetball) | haspet(y,Rat) | haspet(z,Rat). -nextto(x,y) | -samehouse(1,x) | -hasgame(x,Racquetball) | haspet(y,Rat). -nextto(x,y) | -samehouse(x,5) | -hasgame(x,Racquetball) | haspet(y,Rat). % Solitaire is played in the house where Vodka is drunk. -hasgame(x,Solitaire) | hasdrink(x,Vodka). hasgame(x,Solitaire) | -hasdrink(x,Vodka). % The American lives in the house where Charades is played. -hasperson(x,American) | hasgame(x,Charades). hasperson(x,American) | -hasgame(x,Charades). % The Russian lives next to the Blue house. -hasperson(x,Russian) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hascolor(y,Blue) | hascolor(z,Blue). -hasperson(x,Russian) | -samehouse(1,x) | -nextto(x,y) | hascolor(y,Blue). -hasperson(x,Russian) | -samehouse(x,5) | -nextto(x,y) | hascolor(y,Blue). -hasperson(x,Russian) | nextto(x,y) | -hascolor(y,Blue). samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hascolor(x,Blue) | hasperson(y,Russian)| hasperson(z,Russian). -nextto(x,y) | -hascolor(x,Blue) | -samehouse(1,x) | hasperson(y,Russian). -nextto(x,y) | -hascolor(x,Blue) | -samehouse(x,5) | hasperson(y,Russian). % denial: -hasperson(2,x1) | -hasperson(3,x2) | -hasperson(4,x3) | -hasperson(5,x4) | -hascolor(1,x5) | -hascolor(2,x6) | -hascolor(3,x7) | -hascolor(4,x8) | -hascolor(5,x9) | -hasdrink(1,x10) | -hasdrink(2,x11) | -hasdrink(4,x12) | -hasdrink(5,x13) | -hasgame(1,x14) | -hasgame(2,x15) | -hasgame(3,x16) | -hasgame(4,x17) | -hasgame(5,x18) | -haspet(1,x19) | -haspet(2,x20) | -haspet(3,x21) | -haspet(4,x22) | -haspet(5,x23) | SOLVED(PROBLEM,x) | $ANSWER( hasperson(2,x1),hasperson(3,x2),hasperson(4,x3),hasperson(5,x4), hascolor(1,x5),hascolor(2,x6),hascolor(3,x7),hascolor(4,x8), hascolor(5,x9),hasdrink(1,x10),hasdrink(2,x11),hasdrink(4,x12), hasdrink(5,x13),hasgame(1,x14),hasgame(2,x15),hasgame(3,x16), hasgame(4,x17),hasgame(5,x18),haspet(1,x19),haspet(2,x20), haspet(3,x21),haspet(4,x22),haspet(5,x23)). -SOLVED(x,HOUSES). -left(x,1). -left(5,x). left(1,2). left(2,3). left(3,4). left(4,5). -nextto(1,3). -nextto(1,4). -nextto(1,5). -nextto(2,4). -nextto(2,5). -nextto(3,5). % Milk is drunk in the 3rd house. hasdrink(3,Milk). % The Russian lives in the 1st house. hasperson(1,Russian). SHAR_EOF if test -f 'houses.ver1.in' then echo shar: over-writing existing file "'houses.ver1.in'" fi cat << \SHAR_EOF > 'houses.ver1.in' % problem-set/puzzles/miscell/houses.ver1.in % created : 08/02/88 % revised : 08/11/88 % description: % % This run solves "The Houses" puzzle using binary-resolution % and UR-resolution, factoring, unit-deletion, and weighting. % % The Houses % % There are 5 houses, 5 people, 5 colors, 5 drinks, 5 games, % and 4 pets. Each house has a person, a color, a drink, and % game, and all but one of the houses has a pet. The problem % is to match each house with as many properties as possible. % House 1 is at the left end and house 5 is at the right end. % The Englishman lives in the Red house. The White house is % left of the Green house. The Italian has a Guppy. Lemonade % is drunk in the Green house. The Swede lives in the house % where Coffee is drunk. The Toad lives in the house where % Backgammon is played. Racquetball is played in the Yellow % house. Milk is drunk in the third house. The Russian lives % in the first house. The Camel lives next to the house where % Quoits is played. The Rat lives next to the house where % Racquetball is played. Solitaire is played in the house % where Vodka is drunk. The American lives in the house % where Charades is played. The Russian lives next to the Blue % house. % representation: % % Predicates: % samehouse, sameperson, samecolor, samedrink, samegame, and % samepet predicates indicate that both arguments are % identical items. % nextto(x,y) indicates that house x is immediately next to % house y. on either side. % left(x,y) indicates that house x is to the immediate left % of house y. % hasperson, hascolor, hasdrink, hasgame, haspet predicates % indicate that the house identified by the first argument % has the item indicated by the second argument. set(UR_res). set(binary_res). set(factor). set(Unit_deletion). assign(max_weight,999). list(axioms). % definition of samehouse samehouse(x,x). -samehouse(1,2). -samehouse(1,3). -samehouse(1,4). -samehouse(1,5). -samehouse(2,3). -samehouse(2,4). -samehouse(2,5). -samehouse(3,4). -samehouse(3,5). -samehouse(4,5). % definition of sameperson sameperson(x,x). -sameperson(Englishman,Italian). -sameperson(Englishman,Swede). -sameperson(Englishman,Russian). -sameperson(Englishman,American). -sameperson(Italian,Swede). -sameperson(Italian,Russian). -sameperson(Italian,American). -sameperson(Swede,Russian). -sameperson(Swede,American). -sameperson(Russian,American). % definition of samecolor samecolor(x,x). -samecolor(Red,White). -samecolor(Red,Green). -samecolor(Red,Yellow). -samecolor(Red,Blue). -samecolor(White,Green). -samecolor(White,Yellow). -samecolor(White,Blue). -samecolor(Green,Yellow). -samecolor(Green,Blue). -samecolor(Yellow,Blue). % definition of samedrink samedrink(x,x). -samedrink(Lemonade,Coffee). -samedrink(Lemonade,Milk). -samedrink(Lemonade,Vodka). -samedrink(Lemonade,Unknowndrink). -samedrink(Coffee,Milk). -samedrink(Coffee,Vodka). -samedrink(Coffee,Unknowndrink). -samedrink(Milk,Vodka). -samedrink(Milk,Unknowndrink). -samedrink(Vodka,Unknowndrink). % definition of samegame samegame(x,x). -samegame(Backgammon,Racquetball). -samegame(Backgammon,Quoits). -samegame(Backgammon,Solitaire). -samegame(Backgammon,Charades). -samegame(Racquetball,Quoits). -samegame(Racquetball,Solitaire). -samegame(Racquetball,Charades). -samegame(Quoits,Solitaire). -samegame(Quoits,Charades). -samegame(Solitaire,Charades). % definition of samepet samepet(x,x). -samepet(Guppy,Toad). -samepet(Guppy,Camel). -samepet(Guppy,Rat). -samepet(Guppy,No_pet). -samepet(Toad,Camel). -samepet(Toad,Rat). -samepet(Toad,No_pet). -samepet(Camel,Rat). -samepet(Camel,No_pet). -samepet(Rat,No_pet). % Definition and properties of nextto and left -nextto(x,y) | nextto(y,x). -left(x,y) | -left(y,x). -nextto(x,y) | left(x,y) | left(y,x). -left(x,y) | nextto(x,y). -samehouse(x,y) | -nextto(x,y). -left(x,x). -nextto(x,x). % Each house has a person and each person has a house: hasperson(x,Englishman) | hasperson(x,Italian) | hasperson(x,Swede) | hasperson(x,Russian) | hasperson(x,American). hasperson(1,y) | hasperson(2,y) | hasperson(3,y) | hasperson(4,y) | hasperson(5,y). % Each house has a color and each color has a house: hascolor(x,Red) | hascolor(x,White) | hascolor(x,Green) | hascolor(x,Yellow) | hascolor(x,Blue). hascolor(1,y) | hascolor(2,y) | hascolor(3,y) | hascolor(4,y) | hascolor(5,y). % Each house has a drink and each drink has a house: hasdrink(x,Lemonade) | hasdrink(x,Coffee) | hasdrink(x,Milk) | hasdrink(x,Vodka) | hasdrink(x,Unknowndrink). hasdrink(1,y) | hasdrink(2,y) | hasdrink(3,y) | hasdrink(4,y) | hasdrink(5,y). % Each house has a game and each game has a house: hasgame(x,Backgammon) | hasgame(x,Racquetball) | hasgame(x,Quoits) | hasgame(x,Solitaire) | hasgame(x,Charades). hasgame(1,y) | hasgame(2,y) | hasgame(3,y) | hasgame(4,y) | hasgame(5,y). % Each house has a pet and each pet has a house: haspet(x,Guppy) | haspet(x,Toad) | haspet(x,Camel) | haspet(x,Rat) | haspet(x,No_pet). haspet(1,y) | haspet(2,y) | haspet(3,y) | haspet(4,y) | haspet(5,y). % Unique items to each house: samehouse(x1,x2) | -hascolor(x1,y) | -hascolor(x2,y). samehouse(x1,x2) | -hasperson(x1,y) | -hasperson(x2,y). samehouse(x1,x2) | -hasdrink(x1,y) | -hasdrink(x2,y). samehouse(x1,x2) | -hasgame(x1,y) | -hasgame(x2,y). samehouse(x1,x2) | -haspet(x1,y) | -haspet(x2,y). sameperson(x1,x2) | -hasperson(y,x1) | -hasperson(y,x2). samecolor(x1,x2) | -hascolor(y,x1) | -hascolor(y,x2). samedrink(x1,x2) | -hasdrink(y,x1) | -hasdrink(y,x2). samegame(x1,x2) | -hasgame(y,x1) | -hasgame(y,x2). samepet(x1,x2) | -haspet(y,x1) | -haspet(y,x2). % The Englishman lives in the Red house -hasperson(x,Englishman) | hascolor(x,Red). hasperson(x,Englishman) | -hascolor(x,Red). % The White house is left of the Green house. -hascolor(x,White) | -hascolor(y,Green) | left(x,y). -hascolor(x,White) | hascolor(y,Green) | -left(x,y). hascolor(x,White) | -hascolor(y,Green) | -left(x,y). % The Italian has a Guppy. -hasperson(x,Italian) | haspet(x,Guppy). hasperson(x,Italian) | -haspet(x,Guppy). % Lemonade is drunk is the Green house. -hasdrink(x,Lemonade) | hascolor(x,Green). hasdrink(x,Lemonade) | -hascolor(x,Green). % The Swede lives in the house where Coffee is drunk. -hasperson(x,Swede) | hasdrink(x,Coffee). hasperson(x,Swede) | -hasdrink(x,Coffee). % The Toad lives in the house where Backgammon is played. -haspet(x,Toad) | hasgame(x,Backgammon). haspet(x,Toad) | -hasgame(x,Backgammon). % Racquetball is played in the Yellow house. -hasgame(x,Racquetball) | hascolor(x,Yellow). hasgame(x,Racquetball) | -hascolor(x,Yellow). % The Camel lives next to the house where Quoits is played. -haspet(x,Camel) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hasgame(y,Quoits) | hasgame(z,Quoits). -haspet(x,Camel) | -samehouse(1,x) | -nextto(x,y) | hasgame(y,Quoits). -haspet(x,Camel) | -samehouse(x,5) | -nextto(x,y) | hasgame(y,Quoits). -haspet(x,Camel) | nextto(x,y) | -hasgame(y,Quoits). samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Quoits) | haspet(y,Camel) | haspet(z,Camel). -samehouse(1,x) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel). -samehouse(x,5) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel). % The Rat lives next to the house where Racquetball is played. -haspet(x,Rat) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hasgame(y,Racquetball) | hasgame(z,Racquetball). -haspet(x,Rat) | -nextto(x,y) | -samehouse(1,x) | hasgame(y,Racquetball). -haspet(x,Rat) | -nextto(x,y) | -samehouse(x,5) | hasgame(y,Racquetball). -haspet(x,Rat) | nextto(x,y) | -hasgame(y,Racquetball). samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Racquetball) | haspet(y,Rat) | haspet(z,Rat). -nextto(x,y) | -samehouse(1,x) | -hasgame(x,Racquetball) | haspet(y,Rat). -nextto(x,y) | -samehouse(x,5) | -hasgame(x,Racquetball) | haspet(y,Rat). % Solitaire is played in the house where Vodka is drunk. -hasgame(x,Solitaire) | hasdrink(x,Vodka). hasgame(x,Solitaire) | -hasdrink(x,Vodka). % The American lives in the house where Charades is played. -hasperson(x,American) | hasgame(x,Charades). hasperson(x,American) | -hasgame(x,Charades). % The Russian lives next to the Blue house. -hasperson(x,Russian) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hascolor(y,Blue) | hascolor(z,Blue). -hasperson(x,Russian) | -samehouse(1,x) | -nextto(x,y) | hascolor(y,Blue). -hasperson(x,Russian) | -samehouse(x,5) | -nextto(x,y) | hascolor(y,Blue). -hasperson(x,Russian) | nextto(x,y) | -hascolor(y,Blue). samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hascolor(x,Blue) | hasperson(y,Russian)| hasperson(z,Russian). -nextto(x,y) | -hascolor(x,Blue) | -samehouse(1,x) | hasperson(y,Russian). -nextto(x,y) | -hascolor(x,Blue) | -samehouse(x,5) | hasperson(y,Russian). % denial: -hasperson(2,x1) | -hasperson(3,x2) | -hasperson(4,x3) | -hasperson(5,x4) | -hascolor(1,x5) | -hascolor(2,x6) | -hascolor(3,x7) | -hascolor(4,x8) | -hascolor(5,x9) | -hasdrink(1,x10) | -hasdrink(2,x11) | -hasdrink(4,x12) | -hasdrink(5,x13) | -hasgame(1,x14) | -hasgame(2,x15) | -hasgame(3,x16) | -hasgame(4,x17) | -hasgame(5,x18) | -haspet(1,x19) | -haspet(2,x20) | -haspet(3,x21) | -haspet(4,x22) | -haspet(5,x23) | SOLVED(PROBLEM,x) | $ANSWER( hasperson(2,x1),hasperson(3,x2),hasperson(4,x3),hasperson(5,x4), hascolor(1,x5),hascolor(2,x6),hascolor(3,x7),hascolor(4,x8), hascolor(5,x9),hasdrink(1,x10),hasdrink(2,x11),hasdrink(4,x12), hasdrink(5,x13),hasgame(1,x14),hasgame(2,x15),hasgame(3,x16), hasgame(4,x17),hasgame(5,x18),haspet(1,x19),haspet(2,x20), haspet(3,x21),haspet(4,x22),haspet(5,x23)). -SOLVED(x,HOUSES). end_of_list. list(sos). -left(x,1). -left(5,x). left(1,2). left(2,3). left(3,4). left(4,5). -nextto(1,3). -nextto(1,4). -nextto(1,5). -nextto(2,4). -nextto(2,5). -nextto(3,5). % Milk is drunk in the 3rd house. hasdrink(3,Milk). % The Russian lives in the 1st house. hasperson(1,Russian). end_of_list. Weight_list(keep_gen). Weight(PROBLEM, 1000). Weight(HOUSES, 1000). end_of_list. SHAR_EOF if test -f 'houses.ver1.out' then echo shar: over-writing existing file "'houses.ver1.out'" fi cat << \SHAR_EOF > 'houses.ver1.out' OTTER version 0.91, 14 June 1988. set(UR_res). set(binary_res). set(factor). set(Unit_deletion). assign(max_weight,999). list(axioms). 1 samehouse(x,x). 2 -samehouse(1,2). 3 -samehouse(1,3). 4 -samehouse(1,4). 5 -samehouse(1,5). 6 -samehouse(2,3). 7 -samehouse(2,4). 8 -samehouse(2,5). 9 -samehouse(3,4). 10 -samehouse(3,5). 11 -samehouse(4,5). 12 sameperson(x,x). 13 -sameperson(Englishman,Italian). 14 -sameperson(Englishman,Swede). 15 -sameperson(Englishman,Russian). 16 -sameperson(Englishman,American). 17 -sameperson(Italian,Swede). 18 -sameperson(Italian,Russian). 19 -sameperson(Italian,American). 20 -sameperson(Swede,Russian). 21 -sameperson(Swede,American). 22 -sameperson(Russian,American). 23 samecolor(x,x). 24 -samecolor(Red,White). 25 -samecolor(Red,Green). 26 -samecolor(Red,Yellow). 27 -samecolor(Red,Blue). 28 -samecolor(White,Green). 29 -samecolor(White,Yellow). 30 -samecolor(White,Blue). 31 -samecolor(Green,Yellow). 32 -samecolor(Green,Blue). 33 -samecolor(Yellow,Blue). 34 samedrink(x,x). 35 -samedrink(Lemonade,Coffee). 36 -samedrink(Lemonade,Milk). 37 -samedrink(Lemonade,Vodka). 38 -samedrink(Lemonade,Unknowndrink). 39 -samedrink(Coffee,Milk). 40 -samedrink(Coffee,Vodka). 41 -samedrink(Coffee,Unknowndrink). 42 -samedrink(Milk,Vodka). 43 -samedrink(Milk,Unknowndrink). 44 -samedrink(Vodka,Unknowndrink). 45 samegame(x,x). 46 -samegame(Backgammon,Racquetball). 47 -samegame(Backgammon,Quoits). 48 -samegame(Backgammon,Solitaire). 49 -samegame(Backgammon,Charades). 50 -samegame(Racquetball,Quoits). 51 -samegame(Racquetball,Solitaire). 52 -samegame(Racquetball,Charades). 53 -samegame(Quoits,Solitaire). 54 -samegame(Quoits,Charades). 55 -samegame(Solitaire,Charades). 56 samepet(x,x). 57 -samepet(Guppy,Toad). 58 -samepet(Guppy,Camel). 59 -samepet(Guppy,Rat). 60 -samepet(Guppy,No_pet). 61 -samepet(Toad,Camel). 62 -samepet(Toad,Rat). 63 -samepet(Toad,No_pet). 64 -samepet(Camel,Rat). 65 -samepet(Camel,No_pet). 66 -samepet(Rat,No_pet). 67 -nextto(x,y) | nextto(y,x). 68 -left(x,y) | -left(y,x). 69 -nextto(x,y) | left(x,y) | left(y,x). 70 -left(x,y) | nextto(x,y). 71 -samehouse(x,y) | -nextto(x,y). 72 -left(x,x). 73 -nextto(x,x). 74 hasperson(x,Englishman) | hasperson(x,Italian) | hasperson(x,Swede) | hasperson(x,Russian) | hasperson(x,American). 75 hasperson(1,y) | hasperson(2,y) | hasperson(3,y) | hasperson(4,y) | hasperson(5,y). 76 hascolor(x,Red) | hascolor(x,White) | hascolor(x,Green) | hascolor(x,Yellow) | hascolor(x,Blue). 77 hascolor(1,y) | hascolor(2,y) | hascolor(3,y) | hascolor(4,y) | hascolor(5,y). 78 hasdrink(x,Lemonade) | hasdrink(x,Coffee) | hasdrink(x,Milk) | hasdrink(x,Vodka) | hasdrink(x,Unknowndrink). 79 hasdrink(1,y) | hasdrink(2,y) | hasdrink(3,y) | hasdrink(4,y) | hasdrink(5,y). 80 hasgame(x,Backgammon) | hasgame(x,Racquetball) | hasgame(x,Quoits) | hasgame(x,Solitaire) | hasgame(x,Charades). 81 hasgame(1,y) | hasgame(2,y) | hasgame(3,y) | hasgame(4,y) | hasgame(5,y). 82 haspet(x,Guppy) | haspet(x,Toad) | haspet(x,Camel) | haspet(x,Rat) | haspet(x,No_pet). 83 haspet(1,y) | haspet(2,y) | haspet(3,y) | haspet(4,y) | haspet(5,y). 84 samehouse(x1,x2) | -hascolor(x1,y) | -hascolor(x2,y). 85 samehouse(x1,x2) | -hasperson(x1,y) | -hasperson(x2,y). 86 samehouse(x1,x2) | -hasdrink(x1,y) | -hasdrink(x2,y). 87 samehouse(x1,x2) | -hasgame(x1,y) | -hasgame(x2,y). 88 samehouse(x1,x2) | -haspet(x1,y) | -haspet(x2,y). 89 sameperson(x1,x2) | -hasperson(y,x1) | -hasperson(y,x2). 90 samecolor(x1,x2) | -hascolor(y,x1) | -hascolor(y,x2). 91 samedrink(x1,x2) | -hasdrink(y,x1) | -hasdrink(y,x2). 92 samegame(x1,x2) | -hasgame(y,x1) | -hasgame(y,x2). 93 samepet(x1,x2) | -haspet(y,x1) | -haspet(y,x2). 94 -hasperson(x,Englishman) | hascolor(x,Red). 95 hasperson(x,Englishman) | -hascolor(x,Red). 96 -hascolor(x,White) | -hascolor(y,Green) | left(x,y). 97 -hascolor(x,White) | hascolor(y,Green) | -left(x,y). 98 hascolor(x,White) | -hascolor(y,Green) | -left(x,y). 99 -hasperson(x,Italian) | haspet(x,Guppy). 100 hasperson(x,Italian) | -haspet(x,Guppy). 101 -hasdrink(x,Lemonade) | hascolor(x,Green). 102 hasdrink(x,Lemonade) | -hascolor(x,Green). 103 -hasperson(x,Swede) | hasdrink(x,Coffee). 104 hasperson(x,Swede) | -hasdrink(x,Coffee). 105 -haspet(x,Toad) | hasgame(x,Backgammon). 106 haspet(x,Toad) | -hasgame(x,Backgammon). 107 -hasgame(x,Racquetball) | hascolor(x,Yellow). 108 hasgame(x,Racquetball) | -hascolor(x,Yellow). 109 -haspet(x,Camel) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hasgame(y,Quoits) | hasgame(z,Quoits). 110 -haspet(x,Camel) | -samehouse(1,x) | -nextto(x,y) | hasgame(y,Quoits). 111 -haspet(x,Camel) | -samehouse(x,5) | -nextto(x,y) | hasgame(y,Quoits). 112 -haspet(x,Camel) | nextto(x,y) | -hasgame(y,Quoits). 113 samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Quoits) | haspet(y,Camel) | haspet(z,Camel). 114 -samehouse(1,x) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel). 115 -samehouse(x,5) | -nextto(x,y) | -hasgame(x,Quoits) | haspet(y,Camel). 116 -haspet(x,Rat) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hasgame(y,Racquetball) | hasgame(z,Racquetball). 117 -haspet(x,Rat) | -nextto(x,y) | -samehouse(1,x) | hasgame(y,Racquetball). 118 -haspet(x,Rat) | -nextto(x,y) | -samehouse(x,5) | hasgame(y,Racquetball). 119 -haspet(x,Rat) | nextto(x,y) | -hasgame(y,Racquetball). 120 samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hasgame(x,Racquetball) | haspet(y,Rat) | haspet(z,Rat). 121 -nextto(x,y) | -samehouse(1,x) | -hasgame(x,Racquetball) | haspet(y,Rat). 122 -nextto(x,y) | -samehouse(x,5) | -hasgame(x,Racquetball) | haspet(y,Rat). 123 -hasgame(x,Solitaire) | hasdrink(x,Vodka). 124 hasgame(x,Solitaire) | -hasdrink(x,Vodka). 125 -hasperson(x,American) | hasgame(x,Charades). 126 hasperson(x,American) | -hasgame(x,Charades). 127 -hasperson(x,Russian) | samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | hascolor(y,Blue) | hascolor(z,Blue). 128 -hasperson(x,Russian) | -samehouse(1,x) | -nextto(x,y) | hascolor(y,Blue). 129 -hasperson(x,Russian) | -samehouse(x,5) | -nextto(x,y) | hascolor(y,Blue). 130 -hasperson(x,Russian) | nextto(x,y) | -hascolor(y,Blue). 131 samehouse(y,z) | -nextto(x,y) | -nextto(x,z) | -hascolor(x,Blue) | hasperson(y,Russian) | hasperson(z,Russian). 132 -nextto(x,y) | -hascolor(x,Blue) | -samehouse(1,x) | hasperson(y,Russian). 133 -nextto(x,y) | -hascolor(x,Blue) | -samehouse(x,5) | hasperson(y,Russian). 134 -hasperson(2,x1) | -hasperson(3,x2) | -hasperson(4,x3) | -hasperson(5,x4) | -hascolor(1,x5) | -hascolor(2,x6) | -hascolor(3,x7) | -hascolor(4,x8) | -hascolor(5,x9) | -hasdrink(1,x10) | -hasdrink(2,x11) | -hasdrink(4,x12) | -hasdrink(5,x13) | -hasgame(1,x14) | -hasgame(2,x15) | -hasgame(3,x16) | -hasgame(4,x17) | -hasgame(5,x18) | -haspet(1,x19) | -haspet(2,x20) | -haspet(3,x21) | -haspet(4,x22) | -haspet(5,x23) | SOLVED(PROBLEM,x) | $ANSWER(hasperson(2,x1),hasperson(3,x2),hasperson(4,x3),hasperson(5,x4),hascolor(1,x5),hascolor(2,x6),hascolor(3,x7),hascolor(4,x8),hascolor(5,x9),hasdrink(1,x10),hasdrink(2,x11),hasdrink(4,x12),hasdrink(5,x13),hasgame(1,x14),hasgame(2,x15),hasgame(3,x16),hasgame(4,x17),hasgame(5,x18),haspet(1,x19),haspet(2,x20),haspet(3,x21),haspet(4,x22),haspet(5,x23)). 135 -SOLVED(x,HOUSES). end_of_list. list(sos). 136 -left(x,1). 137 -left(5,x). 138 left(1,2). 139 left(2,3). 140 left(3,4). 141 left(4,5). 142 -nextto(1,3). 143 -nextto(1,4). 144 -nextto(1,5). 145 -nextto(2,4). 146 -nextto(2,5). 147 -nextto(3,5). 148 hasdrink(3,Milk). 149 hasperson(1,Russian). end_of_list. Weight_list(keep_gen). Weight(PROBLEM,1000). Weight(HOUSES,1000). end_of_list. ---------------- PROOF ---------------- 1 samehouse(x,x). 2 -samehouse(1,2). 3 -samehouse(1,3). 4 -samehouse(1,4). 6 -samehouse(2,3). 7 -samehouse(2,4). 10 -samehouse(3,5). 15 -sameperson(Englishman,Russian). 16 -sameperson(Englishman,American). 20 -sameperson(Swede,Russian). 21 -sameperson(Swede,American). 22 -sameperson(Russian,American). 24 -samecolor(Red,White). 25 -samecolor(Red,Green). 27 -samecolor(Red,Blue). 30 -samecolor(White,Blue). 32 -samecolor(Green,Blue). 33 -samecolor(Yellow,Blue). 36 -samedrink(Lemonade,Milk). 37 -samedrink(Lemonade,Vodka). 39 -samedrink(Coffee,Milk). 40 -samedrink(Coffee,Vodka). 42 -samedrink(Milk,Vodka). 51 -samegame(Racquetball,Solitaire). 55 -samegame(Solitaire,Charades). 57 -samepet(Guppy,Toad). 59 -samepet(Guppy,Rat). 61 -samepet(Toad,Camel). 62 -samepet(Toad,Rat). 64 -samepet(Camel,Rat). 67 -nextto(x,y) | nextto(y,x). 70 -left(x,y) | nextto(x,y). 71 -samehouse(x,y) | -nextto(x,y). 73 -nextto(x,x). 74 hasperson(x,Englishman) | hasperson(x,Italian) | hasperson(x,Swede) | hasperson(x,Russian) | hasperson(x,American). 76 hascolor(x,Red) | hascolor(x,White) | hascolor(x,Green) | hascolor(x,Yellow) | hascolor(x,Blue). 77 hascolor(1,y) | hascolor(2,y) | hascolor(3,y) | hascolor(4,y) | hascolor(5,y). 78 hasdrink(x,Lemonade) | hasdrink(x,Coffee) | hasdrink(x,Milk) | hasdrink(x,Vodka) | hasdrink(x,Unknowndrink). 79 hasdrink(1,y) | hasdrink(2,y) | hasdrink(3,y) | hasdrink(4,y) | hasdrink(5,y). 80 hasgame(x,Backgammon) | hasgame(x,Racquetball) | hasgame(x,Quoits) | hasgame(x,Solitaire) | hasgame(x,Charades). 81 hasgame(1,y) | hasgame(2,y) | hasgame(3,y) | hasgame(4,y) | hasgame(5,y). 82 haspet(x,Guppy) | haspet(x,Toad) | haspet(x,Camel) | haspet(x,Rat) | haspet(x,No_pet). 83 haspet(1,y) | haspet(2,y) | haspet(3,y) | haspet(4,y) | haspet(5,y). 84 samehouse(x1,x2) | -hascolor(x1,y) | -hascolor(x2,y). 85 samehouse(x1,x2) | -hasperson(x1,y) | -hasperson(x2,y). 86 samehouse(x1,x2) | -hasdrink(x1,y) | -hasdrink(x2,y). 87 samehouse(x1,x2) | -hasgame(x1,y) | -hasgame(x2,y). 88 samehouse(x1,x2) | -haspet(x1,y) | -haspet(x2,y). 89 sameperson(x1,x2) | -hasperson(y,x1) | -hasperson(y,x2). 90 samecolor(x1,x2) | -hascolor(y,x1) | -hascolor(y,x2). 91 samedrink(x1,x2) | -hasdrink(y,x1) | -hasdrink(y,x2). 92 samegame(x1,x2) | -hasgame(y,x1) | -hasgame(y,x2). 93 samepet(x1,x2) | -haspet(y,x1) | -haspet(y,x2). 94 -hasperson(x,Englishman) | hascolor(x,Red). 95 hasperson(x,Englishman) | -hascolor(x,Red). 96 -hascolor(x,White) | -hascolor(y,Green) | left(x,y). 97 -hascolor(x,White) | hascolor(y,Green) | -left(x,y). 98 hascolor(x,White) | -hascolor(y,Green) | -left(x,y). 99 -hasperson(x,Italian) | haspet(x,Guppy). 101 -hasdrink(x,Lemonade) | hascolor(x,Green). 102 hasdrink(x,Lemonade) | -hascolor(x,Green). 103 -hasperson(x,Swede) | hasdrink(x,Coffee). 104 hasperson(x,Swede) | -hasdrink(x,Coffee). 106 haspet(x,Toad) | -hasgame(x,Backgammon). 107 -hasgame(x,Racquetball) | hascolor(x,Yellow). 108 hasgame(x,Racquetball) | -hascolor(x,Yellow). 111 -haspet(x,Camel) | -samehouse(x,5) | -nextto(x,y) | hasgame(y,Quoits). 112 -haspet(x,Camel) | nextto(x,y) | -hasgame(y,Quoits). 119 -haspet(x,Rat) | nextto(x,y) | -hasgame(y,Racquetball). 121 -nextto(x,y) | -samehouse(1,x) | -hasgame(x,Racquetball) | haspet(y,Rat). 123 -hasgame(x,Solitaire) | hasdrink(x,Vodka). 124 hasgame(x,Solitaire) | -hasdrink(x,Vodka). 125 -hasperson(x,American) | hasgame(x,Charades). 126 hasperson(x,American) | -hasgame(x,Charades). 128 -hasperson(x,Russian) | -samehouse(1,x) | -nextto(x,y) | hascolor(y,Blue). 130 -hasperson(x,Russian) | nextto(x,y) | -hascolor(y,Blue). 134 -hasperson(2,x1) | -hasperson(3,x2) | -hasperson(4,x3) | -hasperson(5,x4) | -hascolor(1,x5) | -hascolor(2,x6) | -hascolor(3,x7) | -hascolor(4,x8) | -hascolor(5,x9) | -hasdrink(1,x10) | -hasdrink(2,x11) | -hasdrink(4,x12) | -hasdrink(5,x13) | -hasgame(1,x14) | -hasgame(2,x15) | -hasgame(3,x16) | -hasgame(4,x17) | -hasgame(5,x18) | -haspet(1,x19) | -haspet(2,x20) | -haspet(3,x21) | -haspet(4,x22) | -haspet(5,x23) | SOLVED(PROBLEM,x) | $ANSWER(hasperson(2,x1),hasperson(3,x2),hasperson(4,x3),hasperson(5,x4),hascolor(1,x5),hascolor(2,x6),hascolor(3,x7),hascolor(4,x8),hascolor(5,x9),hasdrink(1,x10),hasdrink(2,x11),hasdrink(4,x12),hasdrink(5,x13),hasgame(1,x14),hasgame(2,x15),hasgame(3,x16),hasgame(4,x17),hasgame(5,x18),haspet(1,x19),haspet(2,x20),haspet(3,x21),haspet(4,x22),haspet(5,x23)). 135 -SOLVED(x,HOUSES). 136 -left(x,1). 138 left(1,2). 139 left(2,3). 140 left(3,4). 141 left(4,5). 142 -nextto(1,3). 144 -nextto(1,5). 145 -nextto(2,4). 148 hasdrink(3,Milk). 149 hasperson(1,Russian). 150 (136,96) -hascolor(x,White) | -hascolor(1,Green). 158 (138,70) nextto(1,2). 161 (139,70) nextto(2,3). 163 (140,98) hascolor(3,White) | -hascolor(4,Green). 164 (140,97) -hascolor(3,White) | hascolor(4,Green). 165 (140,70) nextto(3,4). 167 (141,98) hascolor(4,White) | -hascolor(5,Green). 168 (141,97) -hascolor(4,White) | hascolor(5,Green). 169 (141,70) nextto(4,5). 170 (142,130,149) -hascolor(3,Blue). 184 (144,67) -nextto(5,1). 185 (145,119) -haspet(2,Rat) | -hasgame(4,Racquetball). 188 (145,67) -nextto(4,2). 201 (148,91,39) -hasdrink(3,Coffee). 202 (148,91,36) -hasdrink(3,Lemonade). 204 (148,91,42) -hasdrink(3,Vodka). 205 (148,86,6) -hasdrink(2,Milk). 206 (148,86,3) -hasdrink(1,Milk). 215 (149,130,73) -hascolor(1,Blue). 216 (149,89,20) -hasperson(1,Swede). 218 (149,89,15) -hasperson(1,Englishman). 219 (149,89,22) -hasperson(1,American). 221 (149,85,4) -hasperson(4,Russian). 222 (149,85,3) -hasperson(3,Russian). 223 (149,85,2) -hasperson(2,Russian). 224 (158,128,149,1) hascolor(2,Blue). 225 (158,121,1) -hasgame(1,Racquetball) | haspet(2,Rat). 229 (158,67) nextto(2,1). 240 (161,67) nextto(3,2). 250 (165,67) nextto(4,3). 260 (169,67) nextto(5,4). 282 (184,119) -haspet(5,Rat) | -hasgame(1,Racquetball). 286 (188,112) -haspet(4,Camel) | -hasgame(2,Quoits). 294 (201,103) -hasperson(3,Swede). 296 (202,102) -hascolor(3,Green). 299 (204,123) -hasgame(3,Solitaire). 310 (216,104) -hasdrink(1,Coffee). 314 (218,95) -hascolor(1,Red). 316 (219,126) -hasgame(1,Charades). 343 (224,90,33) -hascolor(2,Yellow). 344 (224,90,32) -hascolor(2,Green). 345 (224,90,30) -hascolor(2,White). 346 (224,90,27) -hascolor(2,Red). 355 (229,71) -samehouse(2,1). 364 (240,71) -samehouse(3,2). 373 (250,71) -samehouse(4,3). 377 (260,111,1) -haspet(5,Camel) | hasgame(4,Quoits). 378 (260,71) -samehouse(5,4). 380 (296,77,344) hascolor(1,Green) | hascolor(4,Green) | hascolor(5,Green). 381 (296,76,170) hascolor(3,Red) | hascolor(3,White) | hascolor(3,Yellow). 392 (343,107) -hasgame(2,Racquetball). 394 (344,101) -hasdrink(2,Lemonade). 396 (344,97,138) -hascolor(1,White). 399 (346,94) -hasperson(2,Englishman). 406 (355,86) -hasdrink(2,x) | -hasdrink(1,x). 415 (364,87) -hasgame(3,x) | -hasgame(2,x). 425 (373,88) -haspet(4,x) | -haspet(3,x). 426 (373,87) -hasgame(4,x) | -hasgame(3,x). 429 (373,84) -hascolor(4,x) | -hascolor(3,x). 436 (378,88) -haspet(5,x) | -haspet(4,x). 448 (394,79,202) hasdrink(1,Lemonade) | hasdrink(4,Lemonade) | hasdrink(5,Lemonade). 449 (394,78,205) hasdrink(2,Coffee) | hasdrink(2,Vodka) | hasdrink(2,Unknowndrink). 451 (396,76,314,215) hascolor(1,Green) | hascolor(1,Yellow). 453 (399,74,223) hasperson(2,Italian) | hasperson(2,Swede) | hasperson(2,American). 462 (150,77,396,345) -hascolor(1,Green) | hascolor(3,White) | hascolor(5,White). 492 (163,90) -hascolor(4,Green) | samecolor(x,White) | -hascolor(3,x). 496 (163,101) hascolor(3,White) | -hasdrink(4,Lemonade). 504 (164,102) -hascolor(3,White) | hasdrink(4,Lemonade). 525 (168,102) -hascolor(4,White) | hasdrink(5,Lemonade). 680 (225,108) haspet(2,Rat) | -hascolor(1,Yellow). 684 (225,185) -hasgame(1,Racquetball) | -hasgame(4,Racquetball). 771 (282,108) -haspet(5,Rat) | -hascolor(1,Yellow). 905 (377,87) -haspet(5,Camel) | samehouse(x,4) | -hasgame(x,Quoits). 1016 (425,99) -haspet(3,Guppy) | -hasperson(4,Italian). 1030 (425,106) -haspet(4,Toad) | -hasgame(3,Backgammon). 1037 (426,125) -hasgame(3,Charades) | -hasperson(4,American). 1051 (426,125) -hasgame(4,Charades) | -hasperson(3,American). 1105 (436,99) -haspet(5,Guppy) | -hasperson(4,Italian). 1178 (451,108) hascolor(1,Green) | hasgame(1,Racquetball). 1237 (504,91) -hascolor(3,White) | samedrink(Lemonade,x) | -hasdrink(4,x). 1256 (525,91) -hascolor(4,White) | samedrink(Lemonade,x) | -hasdrink(5,x). 1362 (680,451) haspet(2,Rat) | hascolor(1,Green). 1419 (771,451) -haspet(5,Rat) | hascolor(1,Green). 1576 (1051,74,294,222) -hasgame(4,Charades) | hasperson(3,Englishman) | hasperson(3,Italian). 1666 (1178,684) hascolor(1,Green) | -hasgame(4,Racquetball). 2788 (462,150) -hascolor(1,Green) | hascolor(5,White). 2826 (2788,150) -hascolor(1,Green). 2830 (2826,1666) -hasgame(4,Racquetball). 2831 (2826,1419) -haspet(5,Rat). 2834 (2826,1362) haspet(2,Rat). 2835 (2826,1178) hasgame(1,Racquetball). 2836 (2826,451) hascolor(1,Yellow). 2837 (2826,380) hascolor(4,Green) | hascolor(5,Green). 2838 (2826,101) -hasdrink(1,Lemonade). 2870 (2834,93,64) -haspet(2,Camel). 2871 (2834,93,62) -haspet(2,Toad). 2872 (2834,93,59) -haspet(2,Guppy). 2881 (2835,92,51) -hasgame(1,Solitaire). 2883 (2835,87,3) -hasgame(3,Racquetball). 2888 (2836,84,3) -hascolor(3,Yellow). 2889 (2838,448) hasdrink(4,Lemonade) | hasdrink(5,Lemonade). 2896 (2871,106) -hasgame(2,Backgammon). 2898 (2872,99) -hasperson(2,Italian). 2903 (2881,124) -hasdrink(1,Vodka). 2904 (2881,81,299) hasgame(2,Solitaire) | hasgame(4,Solitaire) | hasgame(5,Solitaire). 2913 (2883,80,299) hasgame(3,Backgammon) | hasgame(3,Quoits) | hasgame(3,Charades). 2914 (2888,381) hascolor(3,Red) | hascolor(3,White). 2916 (2898,453) hasperson(2,Swede) | hasperson(2,American). 2921 (2903,78,2838,310,206) hasdrink(1,Unknowndrink). 2922 (2921,406) -hasdrink(2,Unknowndrink). 2929 (2922,449) hasdrink(2,Coffee) | hasdrink(2,Vodka). 2932 (2837,163) hascolor(5,Green) | hascolor(3,White). 2941 (2837,167) hascolor(4,Green) | hascolor(4,White). 3041 (2889,496) hasdrink(5,Lemonade) | hascolor(3,White). 3054 (2914,429) hascolor(3,White) | -hascolor(4,Red). 3055 (2914,95) hascolor(3,White) | hasperson(3,Englishman). 3072 (2916,103) hasperson(2,American) | hasdrink(2,Coffee). 3110 (2929,104) hasdrink(2,Vodka) | hasperson(2,Swede). 3114 (2929,86) hasdrink(2,Vodka) | samehouse(2,x) | -hasdrink(x,Coffee). 3115 (2929,124) hasdrink(2,Coffee) | hasgame(2,Solitaire). 3120 (2932,167) hascolor(3,White) | hascolor(4,White). 3312 (3054,164) -hascolor(4,Red) | hascolor(4,Green). 3331 (3055,89) hascolor(3,White) | sameperson(Englishman,x) | -hasperson(3,x). 3376 (3072,91) hasperson(2,American) | samedrink(Coffee,x) | -hasdrink(2,x). 3456 (3110,124) hasperson(2,Swede) | hasgame(2,Solitaire). 3558 (3312,90) -hascolor(4,Red) | samecolor(x,Green) | -hascolor(4,x). 3562 (3558,25) -hascolor(4,Red). 3563 (3562,94) -hasperson(4,Englishman). 3872 (492,94,24) -hascolor(4,Green) | -hasperson(3,Englishman). 3881 (3872,2941) -hasperson(3,Englishman) | hascolor(4,White). 5123 (1237,123,37) -hascolor(3,White) | -hasgame(4,Solitaire). 5151 (5123,3120) -hasgame(4,Solitaire) | hascolor(4,White). 5152 (5123,3055) -hasgame(4,Solitaire) | hasperson(3,Englishman). 5153 (5123,3041) -hasgame(4,Solitaire) | hasdrink(5,Lemonade). 5154 (5123,2932) -hasgame(4,Solitaire) | hascolor(5,Green). 5155 (5123,2914) -hasgame(4,Solitaire) | hascolor(3,Red). 5429 (1256,123,37) -hascolor(4,White) | -hasgame(5,Solitaire). 5461 (5429,3881) -hasgame(5,Solitaire) | -hasperson(3,Englishman). 9095 (3114,7) hasdrink(2,Vodka) | -hasdrink(4,Coffee). 9099 (9095,124) -hasdrink(4,Coffee) | hasgame(2,Solitaire). 9106 (9099,103) hasgame(2,Solitaire) | -hasperson(4,Swede). 10355 (3331,126,16) hascolor(3,White) | -hasgame(3,Charades). 10441 (10355,5123) -hasgame(3,Charades) | -hasgame(4,Solitaire). 10929 (3376,123,40) hasperson(2,American) | -hasgame(2,Solitaire). 10946 (10929,125) -hasgame(2,Solitaire) | hasgame(2,Charades). 10976 (10946,92) -hasgame(2,Solitaire) | samegame(x,Charades) | -hasgame(2,x). 10980 (10976,55) -hasgame(2,Solitaire). 10981 (10980,9106) -hasperson(4,Swede). 10983 (10980,3456) hasperson(2,Swede). 10984 (10980,3115) hasdrink(2,Coffee). 10985 (10980,2904) hasgame(4,Solitaire) | hasgame(5,Solitaire). 10987 (10981,74,3563,221) hasperson(4,Italian) | hasperson(4,American). 10995 (10983,89,21) -hasperson(2,American). 11003 (10995,126) -hasgame(2,Charades). 11006 (11003,80,2896,392,10980) hasgame(2,Quoits). 11009 (11006,905,7) -haspet(5,Camel). 11011 (11006,415) -hasgame(3,Quoits). 11012 (11006,286) -haspet(4,Camel). 11019 (11006,87,7) -hasgame(4,Quoits). 11023 (11009,83,2870,11012) haspet(1,Camel) | haspet(3,Camel). 11029 (11011,2913) hasgame(3,Backgammon) | hasgame(3,Charades). 11057 (10985,5461) hasgame(4,Solitaire) | -hasperson(3,Englishman). 11064 (10987,1105) hasperson(4,American) | -haspet(5,Guppy). 11066 (10987,1016) hasperson(4,American) | -haspet(3,Guppy). 11069 (10987,99) hasperson(4,American) | haspet(4,Guppy). 11079 (10987,125) hasperson(4,Italian) | hasgame(4,Charades). 11233 (11029,1030) hasgame(3,Charades) | -haspet(4,Toad). 11235 (11029,106) hasgame(3,Charades) | haspet(3,Toad). 11250 (11029,10441) hasgame(3,Backgammon) | -hasgame(4,Solitaire). 11367 (11064,125) -haspet(5,Guppy) | hasgame(4,Charades). 11374 (11066,1037) -haspet(3,Guppy) | -hasgame(3,Charades). 11407 (11069,1037) haspet(4,Guppy) | -hasgame(3,Charades). 11410 (11069,125) haspet(4,Guppy) | hasgame(4,Charades). 11669 (11235,10441) haspet(3,Toad) | -hasgame(4,Solitaire). 11826 (11374,11235) -haspet(3,Guppy) | haspet(3,Toad). 11871 (11407,11233) haspet(4,Guppy) | -haspet(4,Toad). 12230 (11826,93) -haspet(3,Guppy) | samepet(x,Toad) | -haspet(3,x). 12234 (12230,57) -haspet(3,Guppy). 12237 (12234,99) -hasperson(3,Italian). 12241 (12237,1576) -hasgame(4,Charades) | hasperson(3,Englishman). 12261 (11871,93) -haspet(4,Toad) | samepet(Guppy,x) | -haspet(4,x). 12266 (12261,57) -haspet(4,Toad). 12268 (12266,106) -hasgame(4,Backgammon). 12348 (12241,80,12268,2830,11019) hasperson(3,Englishman) | hasgame(4,Solitaire). 12753 (12348,11057) hasgame(4,Solitaire). 12763 (12348,5152) hasperson(3,Englishman). 12764 (12753,11669) haspet(3,Toad). 12765 (12753,11250) hasgame(3,Backgammon). 12766 (12753,10441) -hasgame(3,Charades). 12770 (12753,5155) hascolor(3,Red). 12771 (12753,5154) hascolor(5,Green). 12772 (12753,5153) hasdrink(5,Lemonade). 12773 (12753,5151) hascolor(4,White). 12779 (12753,123) hasdrink(4,Vodka). 12784 (12753,92,55) -hasgame(4,Charades). 12794 (12764,93,61) -haspet(3,Camel). 12795 (12764,88,10) -haspet(5,Toad). 12801 (12766,81,316,11003,12784) hasgame(5,Charades). 12842 (12784,11410) haspet(4,Guppy). 12844 (12784,11367) -haspet(5,Guppy). 12845 (12784,11079) hasperson(4,Italian). 12848 (12794,11023) haspet(1,Camel). 12853 (12795,82,12844,11009,2831) haspet(5,No_pet). 12854 (12801,126) hasperson(5,American). 12887 (12853,134,10983,12763,12845,2836,224,12770,12773,12771,2921,10984,12779,12772,2835,11006,12765,12753,12801,12848,2834,12764,12842,135) -hasperson(5,x) | $ANSWER(hasperson(2,Swede),hasperson(3,Englishman),hasperson(4,Italian),hasperson(5,x),hascolor(1,Yellow),hascolor(2,Blue),hascolor(3,Red),hascolor(4,White),hascolor(5,Green),hasdrink(1,Unknowndrink),hasdrink(2,Coffee),hasdrink(4,Vodka),hasdrink(5,Lemonade),hasgame(1,Racquetball),hasgame(2,Quoits),hasgame(3,Backgammon),hasgame(4,Solitaire),hasgame(5,Charades),haspet(1,Camel),haspet(2,Rat),haspet(3,Toad),haspet(4,Guppy),haspet(5,No_pet)). 12888 (12887,12854) $ANSWER(hasperson(2,Swede),hasperson(3,Englishman),hasperson(4,Italian),hasperson(5,American),hascolor(1,Yellow),hascolor(2,Blue),hascolor(3,Red),hascolor(4,White),hascolor(5,Green),hasdrink(1,Unknowndrink),hasdrink(2,Coffee),hasdrink(4,Vodka),hasdrink(5,Lemonade),hasgame(1,Racquetball),hasgame(2,Quoits),hasgame(3,Backgammon),hasgame(4,Solitaire),hasgame(5,Charades),haspet(1,Camel),haspet(2,Rat),haspet(3,Toad),haspet(4,Guppy),haspet(5,No_pet)). --------------- options --------------- set(binary_res). set(UR_res). set(demod_hist). set(for_sub). set(Unit_deletion). set(print_kept). set(factor). 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(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, 999). 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 149 clauses given 1723 clauses generated 92435 demodulation rewrites 0 clauses wt or lit delete 1094 tautologies deleted 1665 clauses forward subsumed 76937 (clauses subsumed by sos) 17247 unit deletions 1363 clauses kept 12739 empty clauses 1 factors generated 3597 clauses back subsumed 10108 clauses not processed 2 ----------- times (seconds) ----------- run time 8515.74 input time 2.09 binary_res time 136.02 hyper_res time 0.00 UR_res time 51.12 para_into time 0.00 para_from time 0.00 pre_process time 7548.76 demod time 0.00 weigh time 85.57 for_sub time 6790.64 unit_del time 449.50 post_process time 959.48 back_sub time 359.95 conflict time 5.50 factor time 256.87 FPA build time 25.36 IS build time 13.68 print_cl time 101.75 cl integrate time 14.22 window time 0.00 SHAR_EOF if test -f 'jobs.desc' then echo shar: over-writing existing file "'jobs.desc'" fi cat << \SHAR_EOF > 'jobs.desc' problem-set/puzzles/miscell/jobs.desc created : 07/09/86 revised : 07/12/88 Natural Language Description: The Jobs Puzzles There are four people: Roberta, Thelma, Steve, and Pete. Among them they hold eight different jobs. Each holds exactly two jobs. The jobs are: chef, guard,nurse, telephone operator,police officer (no gender implied), teacher,actor, and boxer. The job of a nurse is held by a male. The husband of the chef is the telephone operator. Roberta is not a boxer. Pete has no education past the ninth grade. Roberta, the chef, and the police officer went golfing together. Question : Who holds which job ? Versions: jobs.ver1.in : Declarative represention, using UR-resolution created by : W. McCune. verified for ITP : 07/09/86 translated for OTTER by : K.R. verified for OTTER : 07/12/88 SHAR_EOF if test -f 'jobs.ver1.clauses' then echo shar: over-writing existing file "'jobs.ver1.clauses'" fi cat << \SHAR_EOF > 'jobs.ver1.clauses' % problem-set/puzzles/miscell/jobs.ver1.clauses % created : 07/12/88 % revised : 07/12/88 % description: % % This run solves "The Jobs Puzzle" using UR-resolution. % % The Jobs Puzzle % % There are four people: Roberta, Thelma, Steve, and Pete. % Among them they hold eight different jobs. % Each holds exactly two jobs. % The jobs are: chef, guard,nurse, telephone operator,police officer % (no gender implied), teacher, actor, and boxer. % The job of a nurse is held by a male. % The husband of the chef is the telephone operator. % Roberta is not a boxer. % Pete has no education past the ninth grade. % Roberta, the chef, and the police officer went golfing together. % % Question : Who holds which job ? % representation: % % declare_predicate(8,ANSWER). % declare_predicates(2,[HJ,EQP,EQJ,HUSB]). % declare_predicates(1,[EDUCATED,MALE,FEMALE]). % declare_constants([gu,op,po,cte,ac,bo,ch,nu,roberta,thelma,steve,cvince]). % declare_functions(1,[gu1,op1,po1,cte1,ac1,bo1,ch1,nu1]). % declare_variables([u,z,y,x,x1,x2,x3,x4,x5,x6,x7,x8]). % % Predicates: EDUCATED(x) - EDUCATED beyond the ninth grade. % HJ(x,y) - x has the job y. % MALE(x) - person x is a MALE. % FEMALE(x) - person y is a FEMALE. % EQP(x,y) - person x is the same as person y. % EQJ(x,y) - the job x is the same as job y. % HUSB(x,y) - person y is the husband of person x % ANSWER(..) - a predicate to indicate the final answer % % Constants: ch - the chef. % gu - the guard. % op - the telephone operator. % po - the police officer. % cte - the teacher. % ac - the actor. % bo - the boxer. % nu - the nurse. % roberta, thelma, steve, cvince - names of people */ % Every person is the same as himself. % These two clauses eliminate the generation of clauses: -EQP(Rob,Rob) eqp(x,x). eqj(x,x). % Commutative Property -eqp(x,y)| eqp(y,x). -eqj(x,y)| eqj(y,x). % No two people are the same. -eqp(Roberta,Thelma). -eqp(Roberta,Vince). -eqp(Roberta,Steve). -eqp(Vince,Thelma). -eqp(Vince,Steve). % No two jobs are the same. -eqj(CH,GU). -eqj(CH,NU). -eqj(CH,OP). -eqj(CH,PO). -eqj(CH,WA). -eqj(CH,WR). -eqj(CH,TE). -eqj(GU,NU). -eqj(GU,OP). -eqj(GU,PO). -eqj(GU,WA). -eqj(GU,WR). -eqj(GU,TE). -eqj(NU,OP). -eqj(NU,PO). -eqj(NU,WA). -eqj(NU,WR). -eqj(NU,TE). -eqj(OP,PO). -eqj(OP,WA). -eqj(OP,WR). -eqj(OP,TE). -eqj(PO,WA). -eqj(PO,WR). -eqj(PO,TE). -eqj(WA,WR). -eqj(WA,TE). -eqj(WR,TE). % The nurse and actor are MALEs, and the chef is a FEMALE. -hj(x,NU)| male(x). -hj(x,WA)| male(x). -hj(x,CH)| female(x). % The nurse, teacher, and police officer are EDUCATED. -hj(x,NU)| educated(x). -hj(x,TE)| educated(x). -hj(x,PO)| educated(x). % If the person is a chef, she cannot be a police officer. -hj(x,CH)| -hj(x,PO). % Male and FEMALE properties are mutually exclusive of each other. -male(x)| -female(x). male(x)| female(x). % A HUSBand is a MALE and a wife is a FEMALE. -husb(x,y)| male(y). -husb(x,y)| female(x). % The chef and the operator are married. -hj(x,CH)| -hj(y,OP)| husb(x,y). -hj(x,CH)| hj(y,OP)| -husb(x,y). % A job can be held by only one person. -hj(x,z)| -hj(y,z)| eqp(x,y). % If a person can have only 2 unique jobs. -hj(z,u)| -hj(z,x)| -hj(z,y)| eqj(u,x)| eqj(u,y) |eqj(x,y). % A job has to be held by one of roberta, thelma,cvince,steve. hj(Roberta,x) | hj(Thelma,x) | hj(Vince,x) | hj(Steve,x). % A person has to hold one of the given jobs :ch, gu,cte,ac,bo,po,op,nu hj(x,CH) | hj(x,GU) | hj(x,NU) | hj(x,OP) | hj(x,PO) | hj(x,TE) | hj(x,WA) | hj(x,WR). % If all of the listed people have a job then ANSWER gives the result. -hj(x1,CH)| -hj(x2,GU)| -hj(x3,NU)| -hj(x4,OP)| -hj(x5,PO)| -hj(x6,TE)| -hj(x7,WA)| -hj(x8,WR)| $ANS(CHEF(x1),GUARD(x2),NURSE(x3),OPERATOR(x4),POLICE(x5), TEACHER(x6),ACTOR(x7),BOXER(x8)). % Vince has no education past the ninth grade. -educated(Vince). % roberta is not a chef, boxer or police officer since roberta went -hj(Roberta,CH). % golfing with the chef and the police officer. -hj(Roberta,WR). -hj(Roberta,PO). % steve and vince are MALEs (deduced through gender of names), male(Steve). male(Vince). % roberta and thelma are FEMALEs for the same reason. female(Roberta). female(Thelma). SHAR_EOF if test -f 'jobs.ver1.in' then echo shar: over-writing existing file "'jobs.ver1.in'" fi cat << \SHAR_EOF > 'jobs.ver1.in' % problem-set/puzzles/miscell/jobs.ver1.in % created : 07/09/86 % revised : 07/12/88 % description: % % This run solves "The Jobs Puzzle" using UR-resolution. % % The Jobs Puzzle % % There are four people: Roberta, Thelma, Steve, and Pete. % Among them they hold eight different jobs. % Each holds exactly two jobs. % The jobs are: chef, guard,nurse, telephone operator,police officer % (no gender implied), teacher, actor, and boxer. % The job of a nurse is held by a male. % The husband of the chef is the telephone operator. % Roberta is not a boxer. % Pete has no education past the ninth grade. % Roberta, the chef, and the police officer went golfing together. % % Question : Who holds which job ? % representation: % % declare_predicate(8,ANSWER). % declare_predicates(2,[HJ,EQP,EQJ,HUSB]). % declare_predicates(1,[EDUCATED,MALE,FEMALE]). % declare_constants([gu,op,po,cte,ac,bo,ch,nu,roberta,thelma,steve,cvince]). % declare_functions(1,[gu1,op1,po1,cte1,ac1,bo1,ch1,nu1]). % declare_variables([u,z,y,x,x1,x2,x3,x4,x5,x6,x7,x8]). % % Predicates: EDUCATED(x) - EDUCATED beyond the ninth grade. % HJ(x,y) - x has the job y. % MALE(x) - person x is a MALE. % FEMALE(x) - person y is a FEMALE. % EQP(x,y) - person x is the same as person y. % EQJ(x,y) - the job x is the same as job y. % HUSB(x,y) - person y is the husband of person x % ANSWER(..) - a predicate to indicate the final answer % % Constants: ch - the chef. % gu - the guard. % op - the telephone operator. % po - the police officer. % cte - the teacher. % ac - the actor. % bo - the boxer. % nu - the nurse. % roberta, thelma, steve, cvince - names of people */ set(UR_res). list(axioms). % Every person is the same as himself. % These two clauses eliminate the generation of clauses: -EQP(Rob,Rob) eqp(x,x). eqj(x,x). % Commutative Property -eqp(x,y)| eqp(y,x). -eqj(x,y)| eqj(y,x). % No two people are the same. -eqp(Roberta,Thelma). -eqp(Roberta,Vince). -eqp(Roberta,Steve). -eqp(Vince,Thelma). -eqp(Vince,Steve). % No two jobs are the same. -eqj(CH,GU). -eqj(CH,NU). -eqj(CH,OP). -eqj(CH,PO). -eqj(CH,WA). -eqj(CH,WR). -eqj(CH,TE). -eqj(GU,NU). -eqj(GU,OP). -eqj(GU,PO). -eqj(GU,WA). -eqj(GU,WR). -eqj(GU,TE). -eqj(NU,OP). -eqj(NU,PO). -eqj(NU,WA). -eqj(NU,WR). -eqj(NU,TE). -eqj(OP,PO). -eqj(OP,WA). -eqj(OP,WR). -eqj(OP,TE). -eqj(PO,WA). -eqj(PO,WR). -eqj(PO,TE). -eqj(WA,WR). -eqj(WA,TE). -eqj(WR,TE). % The nurse and actor are MALEs, and the chef is a FEMALE. -hj(x,NU)| male(x). -hj(x,WA)| male(x). -hj(x,CH)| female(x). % The nurse, teacher, and police officer are EDUCATED. -hj(x,NU)| educated(x). -hj(x,TE)| educated(x). -hj(x,PO)| educated(x). % If the person is a chef, she cannot be a police officer. -hj(x,CH)| -hj(x,PO). % Male and female properties are mutually exclusive of each other. -male(x)| -female(x). male(x)| female(x). % A HUSBand is a MALE and a wife is a FEMALE. -husb(x,y)| male(y). -husb(x,y)| female(x). % The chef and the operator are married. -hj(x,CH)| -hj(y,OP)| husb(x,y). -hj(x,CH)| hj(y,OP)| -husb(x,y). % A job can be held by only one person. -hj(x,z)| -hj(y,z)| eqp(x,y). % If a person can have only 2 unique jobs. -hj(z,u)| -hj(z,x)| -hj(z,y)| eqj(u,x)| eqj(u,y) |eqj(x,y). % A job has to be held by one of roberta, thelma,cvince,steve. hj(Roberta,x) | hj(Thelma,x) | hj(Vince,x) | hj(Steve,x). % A person has to hold one of the given jobs :ch, gu,cte,ac,bo,po,op,nu hj(x,CH) | hj(x,GU) | hj(x,NU) | hj(x,OP) | hj(x,PO) | hj(x,TE) | hj(x,WA) | hj(x,WR). % If all of the listed people have a job then ANSWER gives the result. -hj(x1,CH)| -hj(x2,GU)| -hj(x3,NU)| -hj(x4,OP)| -hj(x5,PO)| -hj(x6,TE)| -hj(x7,WA)| -hj(x8,WR)| $ANS(CHEF(x1),GUARD(x2),NURSE(x3),OPERATOR(x4),POLICE(x5), TEACHER(x6),ACTOR(x7),BOXER(x8)). end_of_list. list(sos). % Vince has no education past the ninth grade. -educated(Vince). % roberta is not a chef, boxer or police officer since roberta went -hj(Roberta,CH). % golfing with the chef and the police officer. -hj(Roberta,WR). -hj(Roberta,PO). % steve and vince are MALEs (deduced through gender of names), male(Steve). male(Vince). % roberta and thelma are FEMALEs for the same reason. female(Roberta). female(Thelma). end_of_list. SHAR_EOF if test -f 'jobs.ver1.out' then echo shar: over-writing existing file "'jobs.ver1.out'" fi cat << \SHAR_EOF > 'jobs.ver1.out' problem-set/puzzles/miscell/jobs.ver1.out created : 07/12/88 revised : 07/12/88 OTTER version 0.9, 19 May 1988. set(UR_res). list(axioms). 1 eqp(x,x). 2 eqj(x,x). 3 -eqp(x,y) | eqp(y,x). 4 -eqj(x,y) | eqj(y,x). 5 -eqp(Roberta,Thelma). 6 -eqp(Roberta,Vince). 7 -eqp(Roberta,Steve). 8 -eqp(Vince,Thelma). 9 -eqp(Vince,Steve). 10 -eqj(CH,GU). 11 -eqj(CH,NU). 12 -eqj(CH,OP). 13 -eqj(CH,PO). 14 -eqj(CH,WA). 15 -eqj(CH,WR). 16 -eqj(CH,TE). 17 -eqj(GU,NU). 18 -eqj(GU,OP). 19 -eqj(GU,PO). 20 -eqj(GU,WA). 21 -eqj(GU,WR). 22 -eqj(GU,TE). 23 -eqj(NU,OP). 24 -eqj(NU,PO). 25 -eqj(NU,WA). 26 -eqj(NU,WR). 27 -eqj(NU,TE). 28 -eqj(OP,PO). 29 -eqj(OP,WA). 30 -eqj(OP,WR). 31 -eqj(OP,TE). 32 -eqj(PO,WA). 33 -eqj(PO,WR). 34 -eqj(PO,TE). 35 -eqj(WA,WR). 36 -eqj(WA,TE). 37 -eqj(WR,TE). 38 -hj(x,NU) | male(x). 39 -hj(x,WA) | male(x). 40 -hj(x,CH) | female(x). 41 -hj(x,NU) | educated(x). 42 -hj(x,TE) | educated(x). 43 -hj(x,PO) | educated(x). 44 -hj(x,CH) | -hj(x,PO). 45 -male(x) | -female(x). 46 male(x) | female(x). 47 -husb(x,y) | male(y). 48 -husb(x,y) | female(x). 49 -hj(x,CH) | -hj(y,OP) | husb(x,y). 50 -hj(x,CH) | hj(y,OP) | -husb(x,y). 51 -hj(x,z) | -hj(y,z) | eqp(x,y). 52 -hj(z,u) | -hj(z,x) | -hj(z,y) | eqj(u,x) | eqj(u,y) | eqj(x,y). 53 hj(Roberta,x) | hj(Thelma,x) | hj(Vince,x) | hj(Steve,x). 54 hj(x,CH) | hj(x,GU) | hj(x,NU) | hj(x,OP) | hj(x,PO) | hj(x,TE) | hj(x,WA) | hj(x,WR). 55 -hj(x1,CH) | -hj(x2,GU) | -hj(x3,NU) | -hj(x4,OP) | -hj(x5,PO) | -hj(x6,TE) | -hj(x7,WA) | -hj(x8,WR) | $ANS(CHEF(x1),GUARD(x2),NURSE(x3),OPERATOR(x4),POLICE(x5),TEACHER(x6),ACTOR(x7),BOXER(x8)). end_of_list. list(sos). 56 -educated(Vince). 57 -hj(Roberta,CH). 58 -hj(Roberta,WR). 59 -hj(Roberta,PO). 60 male(Steve). 61 male(Vince). 62 female(Roberta). 63 female(Thelma). end_of_list. ---------------- PROOF ---------------- 10 -eqj(CH,GU). 15 -eqj(CH,WR). 16 -eqj(CH,TE). 17 -eqj(GU,NU). 18 -eqj(GU,OP). 19 -eqj(GU,PO). 20 -eqj(GU,WA). 21 -eqj(GU,WR). 23 -eqj(NU,OP). 24 -eqj(NU,PO). 25 -eqj(NU,WA). 26 -eqj(NU,WR). 27 -eqj(NU,TE). 28 -eqj(OP,PO). 29 -eqj(OP,WA). 30 -eqj(OP,WR). 32 -eqj(PO,WA). 33 -eqj(PO,WR). 34 -eqj(PO,TE). 35 -eqj(WA,WR). 37 -eqj(WR,TE). 38 -hj(x,NU) | male(x). 39 -hj(x,WA) | male(x). 40 -hj(x,CH) | female(x). 41 -hj(x,NU) | educated(x). 42 -hj(x,TE) | educated(x). 43 -hj(x,PO) | educated(x). 44 -hj(x,CH) | -hj(x,PO). 45 -male(x) | -female(x). 47 -husb(x,y) | male(y). 49 -hj(x,CH) | -hj(y,OP) | husb(x,y). 52 -hj(z,u) | -hj(z,x) | -hj(z,y) | eqj(u,x) | eqj(u,y) | eqj(x,y). 53 hj(Roberta,x) | hj(Thelma,x) | hj(Vince,x) | hj(Steve,x). 55 -hj(x1,CH) | -hj(x2,GU) | -hj(x3,NU) | -hj(x4,OP) | -hj(x5,PO) | -hj(x6,TE) | -hj(x7,WA) | -hj(x8,WR) | $ANS(CHEF(x1),GUARD(x2),NURSE(x3),OPERATOR(x4),POLICE(x5),TEACHER(x6),ACTOR(x7),BOXER(x8)). 56 -educated(Vince). 57 -hj(Roberta,CH). 58 -hj(Roberta,WR). 59 -hj(Roberta,PO). 60 male(Steve). 61 male(Vince). 62 female(Roberta). 63 female(Thelma). 64 (56,43) -hj(Vince,PO). 65 (56,42) -hj(Vince,TE). 66 (56,41) -hj(Vince,NU). 67 (60,45) -female(Steve). 68 (61,45) -female(Vince). 69 (62,45) -male(Roberta). 70 (63,45) -male(Thelma). 72 (67,40) -hj(Steve,CH). 74 (68,40) -hj(Vince,CH). 75 (69,47) -husb(x,Roberta). 76 (69,39) -hj(Roberta,WA). 77 (69,38) -hj(Roberta,NU). 78 (70,47) -husb(x,Thelma). 79 (70,39) -hj(Thelma,WA). 80 (70,38) -hj(Thelma,NU). 81 (74,53,57,72) hj(Thelma,CH). 82 (80,53,77,66) hj(Steve,NU). 83 (81,49,78) -hj(Thelma,OP). 84 (81,49,75) -hj(Roberta,OP). 85 (81,44) -hj(Thelma,PO). 87 (85,53,59,64) hj(Steve,PO). 88 (87,52,82,17,19,24) -hj(Steve,GU). 89 (87,52,82,23,24,28) -hj(Steve,OP). 90 (87,52,82,24,27,34) -hj(Steve,TE). 91 (87,52,82,24,26,33) -hj(Steve,WR). 92 (87,52,82,24,25,32) -hj(Steve,WA). 93 (89,53,84,83) hj(Vince,OP). 95 (92,53,76,79) hj(Vince,WA). 97 (95,52,93,18,20,29) -hj(Vince,GU). 98 (95,52,93,29,30,35) -hj(Vince,WR). 99 (98,53,58,91) hj(Thelma,WR). 100 (99,52,81,10,15,21) -hj(Thelma,GU). 101 (99,52,81,15,16,37) -hj(Thelma,TE). 102 (100,53,97,88) hj(Roberta,GU). 103 (101,53,65,90) hj(Roberta,TE). 104 (102,55,81,82,93,87,95,99) -hj(x,TE) | $ANS(CHEF(Thelma),GUARD(Roberta),NURSE(Steve),OPERATOR(Vince),POLICE(Steve),TEACHER(x),ACTOR(Vince),BOXER(Thelma)). 105 (104,103) $ANS(CHEF(Thelma),GUARD(Roberta),NURSE(Steve),OPERATOR(Vince),POLICE(Steve),TEACHER(Roberta),ACTOR(Vince),BOXER(Thelma)). --------------- 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 63 clauses given 47 clauses generated 108 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 66 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 42 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 3.50 input time 0.36 binary_res time 0.00 hyper_res time 0.00 UR_res time 2.52 para_into time 0.00 para_from time 0.00 pre_process time 0.34 demod time 0.00 weigh time 0.02 for_sub time 0.20 unit_del time 0.00 post_process time 0.06 back_sub time 0.00 conflict time 0.04 factor time 0.00 FPA build time 0.08 IS build time 0.02 print_cl time 0.18 cl integrate time 0.02 window time 0.00 SHAR_EOF if test -f 'steamroller.desc' then echo shar: over-writing existing file "'steamroller.desc'" fi cat << \SHAR_EOF > 'steamroller.desc' problem-set/puzzles/miscell/steamroller.desc created : 07/09/86 revised : 07/07/88 Natural Language Description: Schubert's Steamroller Puzzle Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also, there are some grains, and grains are plants. Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars, but not snails. Caterpillars and snails like to eat some plants. Show that there is an animal that likes to eat a grain-eating animal. Versions: steamroller.ver1 : declarative representation created by : W. McCune verified for ITP : 07/09/86 translated for OTTER by : K.R. verified for OTTER : 07/07/88 steamroller.ver2 : A special trick has been used to solve this puzzle. A nested function has been used instead of checking (using predicates) whether, for instance, something is an animal and a fox, animal(fox(x)), has been used, even though this is not within the problem. created by : W. McCune verified for ITP : 07/09/86 translated for OTTER by : K.R. verified for OTTER : 07/07/88 SHAR_EOF if test -f 'steamroller.ver1.clauses' then echo shar: over-writing existing file "'steamroller.ver1.clauses'" fi cat << \SHAR_EOF > 'steamroller.ver1.clauses' % problem-set/puzzles/miscell/steamroller.ver1.clauses % created : 07/07/88 % revised : 07/07/88 % description: % % This run solves a puzzle called "Schubert's Steamroller" using % hyper-resolution. % % Schubert's Steamroller Puzzle % % Wolves, foxes, birds, caterpillars, and snails are animals, % and there are some of each of them. % Also, there are some grains, and grains are plants. % Every animal either likes to eat all plants or all animals % much smaller than itself that like to eat some plants. % Caterpillars and snails are much smaller than birds, which % are much are much smaller than foxes, which in turn are % much smaller than wolves. % Wolves do not like to eat foxes or grains, while birds like % to eat caterpillars, but not snails. % Caterpillars and snails like to eat some plants. % Show that there is an animal that likes to eat a grain- % eating animal. % representation: % % declare_predicates(1,[WOLF,ANIMAL,FOX,BIRD,SNAIL,CATERPILLAR]). % declare_predicates(1,[PLANT,GRAIN]). % declare_function(2,f3). % declare_functions(1,[p1,p2]). % declare_predicates(2,[EATS,SMALLER]). % declare_constants([maggie,lupo,foxy,stalky,tweety,slimey]). % declare_variables([x,y,x1,x2,x3,x4]). -WOLF(x1) | ANIMAL(x1). -FOX(x1) | ANIMAL(x1). -BIRD(x1) | ANIMAL(x1). -CATERPILLAR(x1) | ANIMAL(x1). -SNAIL(x1) | ANIMAL(x1). -GRAIN(x1) | PLANT(x1). -ANIMAL(x1) | -PLANT(x2) | -ANIMAL(x3) | -SMALLER(x3,x1) | -PLANT(x4) | -EATS(x3,x4) | EATS(x1,x2) | EATS(x1,x3). -CATERPILLAR(x1) | -BIRD(x2) | SMALLER(x1,x2). -SNAIL(x1) | -BIRD(x2) | SMALLER(x1,x2). -BIRD(x1) | -FOX(x2) | SMALLER(x1,x2). -FOX(x1) | -WOLF(x2) | SMALLER(x1,x2). -BIRD(x1) | -CATERPILLAR(x2) | EATS(x1,x2). -CATERPILLAR(x1) | PLANT(p1(x1)). -CATERPILLAR(x1) | EATS(x1,p1(x1)). -SNAIL(x1) | PLANT(p2(x1)). -SNAIL(x1) | EATS(x1,p2(x1)). -WOLF(x1) | -FOX(x2) | -EATS(x1,x2). -WOLF(x1) | -GRAIN(x2) | -EATS(x1,x2). -BIRD(x1) | -SNAIL(x2) | -EATS(x1,x2). -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | GRAIN(f3(y,x)). -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | -EATS(y,f3(y,x)). WOLF(Lupo). FOX(Foxy). BIRD(Tweety). CATERPILLAR(Maggie). SNAIL(Slimey). GRAIN(Stalky). SHAR_EOF if test -f 'steamroller.ver1.in' then echo shar: over-writing existing file "'steamroller.ver1.in'" fi cat << \SHAR_EOF > 'steamroller.ver1.in' % problem-set/puzzles/miscell/steamroller.ver1.in % created : 07/09/86 % revised : 07/07/88 % description: % % This run solves a puzzle called "Schubert's Steamroller" using % hyper-resolution. % % Schubert's Steamroller Puzzle % % Wolves, foxes, birds, caterpillars, and snails are animals, % and there are some of each of them. % Also, there are some grains, and grains are plants. % Every animal either likes to eat all plants or all animals % much smaller than itself that like to eat some plants. % Caterpillars and snails are much smaller than birds, which % are much are much smaller than foxes, which in turn are % much smaller than wolves. % Wolves do not like to eat foxes or grains, while birds like % to eat caterpillars, but not snails. % Caterpillars and snails like to eat some plants. % Show that there is an animal that likes to eat a grain- % eating animal. % representation: % % declare_predicates(1,[WOLF,ANIMAL,FOX,BIRD,SNAIL,CATERPILLAR]). % declare_predicates(1,[PLANT,GRAIN]). % declare_function(2,f3). % declare_functions(1,[p1,p2]). % declare_predicates(2,[EATS,SMALLER]). % declare_constants([maggie,lupo,foxy,stalky,tweety,slimey]). % declare_variables([x,y,x1,x2,x3,x4]). % % Declarative version using hyper-resolution. set(hyper_res). list(axioms). -WOLF(x1) | ANIMAL(x1). -FOX(x1) | ANIMAL(x1). -BIRD(x1) | ANIMAL(x1). -CATERPILLAR(x1) | ANIMAL(x1). -SNAIL(x1) | ANIMAL(x1). -GRAIN(x1) | PLANT(x1). -ANIMAL(x1) | -PLANT(x2) | -ANIMAL(x3) | -SMALLER(x3,x1) | -PLANT(x4) | -EATS(x3,x4) | EATS(x1,x2) | EATS(x1,x3). -CATERPILLAR(x1) | -BIRD(x2) | SMALLER(x1,x2). -SNAIL(x1) | -BIRD(x2) | SMALLER(x1,x2). -BIRD(x1) | -FOX(x2) | SMALLER(x1,x2). -FOX(x1) | -WOLF(x2) | SMALLER(x1,x2). -BIRD(x1) | -CATERPILLAR(x2) | EATS(x1,x2). -CATERPILLAR(x1) | PLANT(p1(x1)). -CATERPILLAR(x1) | EATS(x1,p1(x1)). -SNAIL(x1) | PLANT(p2(x1)). -SNAIL(x1) | EATS(x1,p2(x1)). -WOLF(x1) | -FOX(x2) | -EATS(x1,x2). -WOLF(x1) | -GRAIN(x2) | -EATS(x1,x2). -BIRD(x1) | -SNAIL(x2) | -EATS(x1,x2). -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | GRAIN(f3(y,x)). -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | -EATS(y,f3(y,x)). end_of_list. list(sos). WOLF(Lupo). FOX(Foxy). BIRD(Tweety). CATERPILLAR(Maggie). SNAIL(Slimey). GRAIN(Stalky). end_of_list. SHAR_EOF if test -f 'steamroller.ver1.out' then echo shar: over-writing existing file "'steamroller.ver1.out'" fi cat << \SHAR_EOF > 'steamroller.ver1.out' problem-set/puzzles/miscell/steamroller.ver1.out created : 07/07/88 revised : 07/07/88 OTTER release 0.9, 19 May 1988 set(hyper_res). list(axioms). 1 -WOLF(x1) | ANIMAL(x1). 2 -FOX(x1) | ANIMAL(x1). 3 -BIRD(x1) | ANIMAL(x1). 4 -CATERPILLAR(x1) | ANIMAL(x1). 5 -SNAIL(x1) | ANIMAL(x1). 6 -GRAIN(x1) | PLANT(x1). 7 -ANIMAL(x1) | -PLANT(x2) | -ANIMAL(x3) | -SMALLER(x3,x1) | -PLANT(x4) | -EATS(x3,x4) | EATS(x1,x2) | EATS(x1,x3). 8 -CATERPILLAR(x1) | -BIRD(x2) | SMALLER(x1,x2). 9 -SNAIL(x1) | -BIRD(x2) | SMALLER(x1,x2). 10 -BIRD(x1) | -FOX(x2) | SMALLER(x1,x2). 11 -FOX(x1) | -WOLF(x2) | SMALLER(x1,x2). 12 -BIRD(x1) | -CATERPILLAR(x2) | EATS(x1,x2). 13 -CATERPILLAR(x1) | PLANT(p1(x1)). 14 -CATERPILLAR(x1) | EATS(x1,p1(x1)). 15 -SNAIL(x1) | PLANT(p2(x1)). 16 -SNAIL(x1) | EATS(x1,p2(x1)). 17 -WOLF(x1) | -FOX(x2) | -EATS(x1,x2). 18 -WOLF(x1) | -GRAIN(x2) | -EATS(x1,x2). 19 -BIRD(x1) | -SNAIL(x2) | -EATS(x1,x2). 20 -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | GRAIN(f3(y,x)). 21 -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | -EATS(y,f3(y,x)). end_of_list. list(sos). 22 WOLF(Lupo). 23 FOX(Foxy). 24 BIRD(Tweety). 25 CATERPILLAR(Maggie). 26 SNAIL(Slimey). 27 GRAIN(Stalky). end_of_list. ---------------- PROOF ---------------- 1 -WOLF(x1) | ANIMAL(x1). 2 -FOX(x1) | ANIMAL(x1). 3 -BIRD(x1) | ANIMAL(x1). 5 -SNAIL(x1) | ANIMAL(x1). 6 -GRAIN(x1) | PLANT(x1). 7 -ANIMAL(x1) | -PLANT(x2) | -ANIMAL(x3) | -SMALLER(x3,x1) | -PLANT(x4) | -EATS(x3,x4) | EATS(x1,x2) | EATS(x1,x3). 9 -SNAIL(x1) | -BIRD(x2) | SMALLER(x1,x2). 10 -BIRD(x1) | -FOX(x2) | SMALLER(x1,x2). 11 -FOX(x1) | -WOLF(x2) | SMALLER(x1,x2). 15 -SNAIL(x1) | PLANT(p2(x1)). 16 -SNAIL(x1) | EATS(x1,p2(x1)). 17 -WOLF(x1) | -FOX(x2) | -EATS(x1,x2). 18 -WOLF(x1) | -GRAIN(x2) | -EATS(x1,x2). 19 -BIRD(x1) | -SNAIL(x2) | -EATS(x1,x2). 20 -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | GRAIN(f3(y,x)). 21 -ANIMAL(x) | -ANIMAL(y) | -EATS(x,y) | -EATS(y,f3(y,x)). 22 WOLF(Lupo). 23 FOX(Foxy). 24 BIRD(Tweety). 26 SNAIL(Slimey). 27 GRAIN(Stalky). 28 (22,1) ANIMAL(Lupo). 29 (23,11,22) SMALLER(Foxy,Lupo). 30 (23,2) ANIMAL(Foxy). 31 (24,10,23) SMALLER(Tweety,Foxy). 32 (24,3) ANIMAL(Tweety). 38 (26,16) EATS(Slimey,p2(Slimey)). 39 (26,15) PLANT(p2(Slimey)). 40 (26,9,24) SMALLER(Slimey,Tweety). 41 (26,5) ANIMAL(Slimey). 42 (27,6) PLANT(Stalky). 44 (38,7,32,42,41,40,39) EATS(Tweety,Stalky) | EATS(Tweety,Slimey). 54 (44,19,24,26) EATS(Tweety,Stalky). 56 (54,7,30,42,32,31,42) EATS(Foxy,Stalky) | EATS(Foxy,Tweety). 60 (56,7,28,42,30,29,42) EATS(Foxy,Tweety) | EATS(Lupo,Stalky) | EATS(Lupo,Foxy). 87 (60,18,22,27) EATS(Foxy,Tweety) | EATS(Lupo,Foxy). 92 (87,17,22,23) EATS(Foxy,Tweety). 93 (92,20,30,32) GRAIN(f3(Tweety,Foxy)). 94 (93,6) PLANT(f3(Tweety,Foxy)). 95 (94,7,32,41,40,39,38) EATS(Tweety,f3(Tweety,Foxy)) | EATS(Tweety,Slimey). 96 (95,21,30,32,92) EATS(Tweety,Slimey). 100 (96,19,24,26) . --------------- 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). 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 27 clauses given 48 clauses generated 189 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 116 (clauses subsumed by sos) 48 unit deletions 0 clauses kept 73 empty clauses 1 factors generated 0 clauses back subsumed 45 clauses not processed 2 ----------- times (seconds) ----------- run time 9.81 input time 0.30 binary_res time 0.00 hyper_res time 7.50 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 1.03 demod time 0.00 weigh time 0.02 for_sub time 0.39 unit_del time 0.00 post_process time 0.54 back_sub time 0.17 conflict time 0.04 factor time 0.00 FPA build time 0.15 IS build time 0.06 print_cl time 0.71 cl integrate time 0.06 window time 0.00 SHAR_EOF if test -f 'steamroller.ver2.clauses' then echo shar: over-writing existing file "'steamroller.ver2.clauses'" fi cat << \SHAR_EOF > 'steamroller.ver2.clauses' % problem-set/puzzles/miscell/steamroller.ver2.clauses % created : 07/07/88 % revised : 07/07/88 % description: % % This run solves "Schubert's Steamroller Puzzle" using UR-resolution. % % Schubert's Steamroller Puzzle % % Wolves, foxes, birds, caterpillars, and snails are animals, % and there are some of each of them. % Also, there are some grains, and grains are plants. % Every animal either likes to eat all plants or all animals much % smaller than itself that like to eat some plants. % Caterpillars and snails are much smaller than birds, which are % much are much smaller than foxes, which in turn are much % smaller than wolves. % Wolves do not like to eat foxes or grains, while birds like to % eat caterpillars, but not snails. % Caterpillars and snails like to eat some plants. % Show that there is an animal that likes to eat a grain-eating % animal. % representation: % % A special trick has been used to solve this puzzle. % Instead of checking (using predicates) whether, for instance, % something is an animal and a fox, animal(fox(x)) has been used as a % nested function, even though this is not within the problem. -Smaller(animal(x3),animal(x1))| -eats(animal(x3),plant(x4)) | eats(animal(x1),plant(x2))| eats(animal(x1),animal(x3)). -eats(animal(x),animal(y))| -eats(animal(y),plant(Grain(z))). -eats(animal(Wolf(x1)),animal(Fox(x2))). -eats(animal(Wolf(x1)),plant(Grain(x2))). -eats(animal(Bird(x1)),animal(Snail(x2))). eats(animal(Bird(x1)),animal(Caterpillar(x2))). eats(animal(Caterpillar(x1)),plant(p1(animal(Caterpillar(x1))))). eats(animal(Snail(x1)),plant(p2(animal(Snail(x1))))). Smaller(animal(Caterpillar(x1)),animal(Bird(x2))). Smaller(animal(Snail(x1)),animal(Bird(x2))). Smaller(animal(Bird(x1)),animal(Fox(x2))). Smaller(animal(Fox(x1)),animal(Wolf(x2))). Grain(Stalky). SHAR_EOF if test -f 'steamroller.ver2.in' then echo shar: over-writing existing file "'steamroller.ver2.in'" fi cat << \SHAR_EOF > 'steamroller.ver2.in' % problem-set/puzzles/miscell/steamroller.ver2.in % created : 07/09/86 % revised : 07/07/88 % description: % % This run solves "Schubert's Steamroller Puzzle" using UR-resolution. % % Schubert's Steamroller Puzzle % % Wolves, foxes, birds, caterpillars, and snails are animals, % and there are some of each of them. % Also, there are some grains, and grains are plants. % Every animal either likes to eat all plants or all animals much % smaller than itself that like to eat some plants. % Caterpillars and snails are much smaller than birds, which are % much are much smaller than foxes, which in turn are much % smaller than wolves. % Wolves do not like to eat foxes or grains, while birds like to % eat caterpillars, but not snails. % Caterpillars and snails like to eat some plants. % Show that there is an animal that likes to eat a grain-eating % animal. % representation: % % A special trick has been used to solve this puzzle. % Instead of checking (using predicates) whether, for instance, % something is an animal and a fox, animal(fox(x)) has been used as a % nested function, even though this is not within the problem. set(UR_res). list(axioms). -Smaller(animal(x3),animal(x1))| -eats(animal(x3),plant(x4)) | eats(animal(x1),plant(x2))| eats(animal(x1),animal(x3)). -eats(animal(x),animal(y))| -eats(animal(y),plant(Grain(z))). -eats(animal(Wolf(x1)),animal(Fox(x2))). -eats(animal(Wolf(x1)),plant(Grain(x2))). -eats(animal(Bird(x1)),animal(Snail(x2))). eats(animal(Bird(x1)),animal(Caterpillar(x2))). eats(animal(Caterpillar(x1)),plant(p1(animal(Caterpillar(x1))))). eats(animal(Snail(x1)),plant(p2(animal(Snail(x1))))). end_of_list. list(sos). Smaller(animal(Caterpillar(x1)),animal(Bird(x2))). Smaller(animal(Snail(x1)),animal(Bird(x2))). Smaller(animal(Bird(x1)),animal(Fox(x2))). Smaller(animal(Fox(x1)),animal(Wolf(x2))). Grain(Stalky). end_of_list. SHAR_EOF if test -f 'steamroller.ver2.out' then echo shar: over-writing existing file "'steamroller.ver2.out'" fi cat << \SHAR_EOF > 'steamroller.ver2.out' problem-set/puzzles/miscell/steamroller.ver2.out created : 07/07/88 revised : 07/07/88 OTTER release 0.9, 19 May 1988 set(UR_res). list(axioms). 1 -Smaller(animal(x3),animal(x1)) | -eats(animal(x3),plant(x4)) | eats(animal(x1),plant(x2)) | eats(animal(x1),animal(x3)). 2 -eats(animal(x),animal(y)) | -eats(animal(y),plant(Grain(z))). 3 -eats(animal(Wolf(x1)),animal(Fox(x2))). 4 -eats(animal(Wolf(x1)),plant(Grain(x2))). 5 -eats(animal(Bird(x1)),animal(Snail(x2))). 6 eats(animal(Bird(x1)),animal(Caterpillar(x2))). 7 eats(animal(Caterpillar(x1)),plant(p1(animal(Caterpillar(x1))))). 8 eats(animal(Snail(x1)),plant(p2(animal(Snail(x1))))). end_of_list. list(sos). 9 Smaller(animal(Caterpillar(x1)),animal(Bird(x2))). 10 Smaller(animal(Snail(x1)),animal(Bird(x2))). 11 Smaller(animal(Bird(x1)),animal(Fox(x2))). 12 Smaller(animal(Fox(x1)),animal(Wolf(x2))). 13 Grain(Stalky). end_of_list. ---------------- PROOF ---------------- 1 -Smaller(animal(x3),animal(x1)) | -eats(animal(x3),plant(x4)) | eats(animal(x1),plant(x2)) | eats(animal(x1),animal(x3)). 2 -eats(animal(x),animal(y)) | -eats(animal(y),plant(Grain(z))). 3 -eats(animal(Wolf(x1)),animal(Fox(x2))). 4 -eats(animal(Wolf(x1)),plant(Grain(x2))). 5 -eats(animal(Bird(x1)),animal(Snail(x2))). 8 eats(animal(Snail(x1)),plant(p2(animal(Snail(x1))))). 10 Smaller(animal(Snail(x1)),animal(Bird(x2))). 11 Smaller(animal(Bird(x1)),animal(Fox(x2))). 12 Smaller(animal(Fox(x1)),animal(Wolf(x2))). 14 (10,1,8,5) eats(animal(Bird(x)),plant(y)). 15 (14,2) -eats(animal(x),animal(Bird(y))). 17 (11,1,14,15) eats(animal(Fox(x)),plant(y)). 19 (17,1,4,3) -Smaller(animal(Fox(x)),animal(Wolf(y))). 20 (19,12) . --------------- 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 13 clauses given 7 clauses generated 7 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 7 empty clauses 1 factors generated 0 clauses back subsumed 1 clauses not processed 3 ----------- times (seconds) ----------- run time 0.48 input time 0.19 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.08 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.01 unit_del time 0.00 post_process time 0.03 back_sub time 0.01 conflict time 0.01 factor time 0.00 FPA build time 0.03 IS build time 0.01 print_cl time 0.11 cl integrate time 0.02 window time 0.00 SHAR_EOF # End of shell archive exit 0