#!/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 # tandl.desc # tandl.ver1.clauses # tandl.ver1.in # tandl.ver1.out # tandl27.desc # tandl27.ver1.clauses # tandl27.ver1.in # tandl27.ver1.out # tandl31.desc # tandl31.ver1.clauses # tandl31.ver1.in # tandl31.ver1.out # tandl35.desc # tandl35.ver1.clauses # tandl35.ver1.in # tandl35.ver1.out # tandl39.desc # tandl39.ver1.clauses # tandl39.ver1.in # tandl39.ver1.out # tandl42.desc # tandl42.ver1.clauses # tandl42.ver1.in # tandl42.ver1.out # This archive created: Tue Aug 16 11:24:59 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/truth.lies/README created : 07/26/86 revised : 07/26/88 Contents of 'truth.lies' : -------------------------- Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/puzzles/truth.lies. tandl : to solve "The Truthtellers and the Liars" puzzle tandl27 : to solve "Truthtellers and Liars Puzzle #27" tandl31 : to solve "Truthtellers and Liars Puzzle #31" tandl35 : to solve "Truthtellers and Liars Puzzle #35" tandl39 : to solve "Truthtellers and Liars Puzzle #39" tandl42 : to solve "Truthtellers and Liars Puzzle #42" ---------------------------------------------------------------------- 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 'tandl.desc' then echo shar: over-writing existing file "'tandl.desc'" fi cat << \SHAR_EOF > 'tandl.desc' problem-set/puzzles/truth_lies/tandl.desc created : 07/09/86 revised : 07/18/88 Natural Language Description: The Truthtellers and the Liars On a certain island the inhabitants are partitioned into those who always tell the truth and those who always lie. I landed on the island and met three inhabitants A, B, and C. I asked A, "Are you a truth-teller or a liar?" He mumbled something which I couldn't make out. I asked B what A had said. B replied, "A said he was a liar." C then volun- teered, "Don't believe B, he's lying!" What can you tell about A, B, and C? Versions: tandl.ver1 : Delarative representation, using hyper-resolution. answer: A is unknown, B is a liar, and C is a truth-teller. created by : E. Lusk verified for ITP : 07/09/86 translated for OTTER by : K.R. verified for OTTER : 07/18/88 SHAR_EOF if test -f 'tandl.ver1.clauses' then echo shar: over-writing existing file "'tandl.ver1.clauses'" fi cat << \SHAR_EOF > 'tandl.ver1.clauses' % problem-set/puzzles/truth_lies/tandl.ver1.clauses % created : 07/13/88 % revised : 07/13/88 % description: % % This run solves the "Truthtellers and the Liars" puzzle using % hyper-resolution. % % Truthtellers and the Liars % % On a certain island the inhabitants are partitioned into % those who always tell the truth and those who always lie. I % landed on the island and met three inhabitants A, B, and C. % I asked A, "Are you a truth-teller or a liar?" He mumbled % something which I couldn't make out. I asked B what A had % said. B replied, "A said he was a liar." C then volun- % teered, "Don't believe B, he's lying!" What can you tell % about A, B, and C? % representation: % % declare_predicate(1,P). % declare_functions(1,[t,l]). % declare_function(2,says). % declare_variables([x,y]). % declare_constants([a,b,c,notknown]). % % P(x) means "x is true". % T(x) means "x is a truthteller". % L(x) means "x is a liar". % Says(x,y) = x makes a statement y. P(T(x)) | P(L(x)). -P(T(x)) | -P(L(x)). -P(T(x)) | -P(Says(x,y)) | P(y). -P(y) | -P(Says(x,y)) | P(T(x)). % if P(L(x)) & P(Says(x,y)) then -P(y). (dependent axiom) % if -P(y) & P(Says(x,y)) then P(L(x)). (dependent axiom) P(Says(A,Unknown)). P(Says(B,Says(A,L(A)))). P(Says(C,L(B))). SHAR_EOF if test -f 'tandl.ver1.in' then echo shar: over-writing existing file "'tandl.ver1.in'" fi cat << \SHAR_EOF > 'tandl.ver1.in' % problem-set/puzzles/truth_lies/tandl.ver1.in % created : 07/09/86 % revised : 07/13/88 % description: % % This run solves the "Truthtellers and the Liars" puzzle using % hyper-resolution. % % Truthtellers and the Liars % % On a certain island the inhabitants are partitioned into % those who always tell the truth and those who always lie. I % landed on the island and met three inhabitants A, B, and C. % I asked A, "Are you a truth-teller or a liar?" He mumbled % something which I couldn't make out. I asked B what A had % said. B replied, "A said he was a liar." C then volun- % teered, "Don't believe B, he's lying!" What can you tell % about A, B, and C? % representation: % % declare_predicate(1,P). % declare_functions(1,[t,l]). % declare_function(2,says). % declare_variables([x,y]). % declare_constants([a,b,c,notknown]). % % P(x) means "x is true". % T(x) means "x is a truthteller". % L(x) means "x is a liar". % Says(x,y) = x makes a statement y. set(hyper_res). list(axioms). P(T(x)) | P(L(x)). -P(T(x)) | -P(L(x)). -P(T(x)) | -P(Says(x,y)) | P(y). -P(y) | -P(Says(x,y)) | P(T(x)). % if P(L(x)) & P(Says(x,y)) then -P(y). (dependent axiom) % if -P(y) & P(Says(x,y)) then P(L(x)). (dependent axiom) end_of_list. list(sos). P(Says(A,Unknown)). P(Says(B,Says(A,L(A)))). P(Says(C,L(B))). end_of_list. SHAR_EOF if test -f 'tandl.ver1.out' then echo shar: over-writing existing file "'tandl.ver1.out'" fi cat << \SHAR_EOF > 'tandl.ver1.out' problem-set/puzzles/truth_lies/tandl.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 P(T(x)) | P(L(x)). 2 -P(T(x)) | -P(L(x)). 3 -P(T(x)) | -P(Says(x,y)) | P(y). 4 -P(y) | -P(Says(x,y)) | P(T(x)). end_of_list. list(sos). 5 P(Says(A,Unknown)). 6 P(Says(B,Says(A,L(A)))). 7 P(Says(C,L(B))). end_of_list. new given clause: 5 P(Says(A,Unknown)). ** KEPT: 8 (5,3,1) P(Unknown) | P(L(A)). new given clause: 7 P(Says(C,L(B))). ** KEPT: 9 (7,4,1) P(T(C)) | P(T(B)). ** KEPT: 10 (7,3,1) P(L(B)) | P(L(C)). new given clause: 8 (5,3,1) P(Unknown) | P(L(A)). new given clause: 9 (7,4,1) P(T(C)) | P(T(B)). new given clause: 10 (7,3,1) P(L(B)) | P(L(C)). new given clause: 6 P(Says(B,Says(A,L(A)))). ** KEPT: 11 (6,3,9) P(Says(A,L(A))) | P(T(C)). ** KEPT: 12 (6,3,1) P(Says(A,L(A))) | P(L(B)). new given clause: 11 (6,3,9) P(Says(A,L(A))) | P(T(C)). ** KEPT: 13 (11,4,8) P(T(C)) | P(T(A)) | P(Unknown). ** KEPT: 14 (11,4,1) P(T(C)) | P(T(A)). ** KEPT: 15 (11,3,1) P(T(C)) | P(L(A)). 14 back subsumes: 13 (11,4,8) P(T(C)) | P(T(A)) | P(Unknown). new given clause: 14 (11,4,1) P(T(C)) | P(T(A)). ** KEPT: 16 (14,3,7) P(T(A)) | P(L(B)). ** KEPT: 17 (14,3,5) P(T(C)) | P(Unknown). new given clause: 17 (14,3,5) P(T(C)) | P(Unknown). ** KEPT: 18 (17,3,7) P(Unknown) | P(L(B)). new given clause: 18 (17,3,7) P(Unknown) | P(L(B)). new given clause: 15 (11,3,1) P(T(C)) | P(L(A)). ** KEPT: 19 (15,3,7) P(L(A)) | P(L(B)). ** KEPT: 20 (15,2,14) P(T(C)). 20 back subsumes: 17 (14,3,5) P(T(C)) | P(Unknown). 20 back subsumes: 15 (11,3,1) P(T(C)) | P(L(A)). 20 back subsumes: 14 (11,4,1) P(T(C)) | P(T(A)). 20 back subsumes: 11 (6,3,9) P(Says(A,L(A))) | P(T(C)). 20 back subsumes: 9 (7,4,1) P(T(C)) | P(T(B)). new given clause: 20 (15,2,14) P(T(C)). ** KEPT: 21 (20,3,7) P(L(B)). 21 back subsumes: 19 (15,3,7) P(L(A)) | P(L(B)). 21 back subsumes: 18 (17,3,7) P(Unknown) | P(L(B)). 21 back subsumes: 16 (14,3,7) P(T(A)) | P(L(B)). 21 back subsumes: 12 (6,3,1) P(Says(A,L(A))) | P(L(B)). 21 back subsumes: 10 (7,3,1) P(L(B)) | P(L(C)). new given clause: 21 (20,3,7) P(L(B)). ------------ END OF SEARCH ------------ sos empty. --------------- 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 7 clauses given 13 clauses generated 48 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 34 (clauses subsumed by sos) 10 unit deletions 0 clauses kept 14 empty clauses 0 factors generated 0 clauses back subsumed 11 clauses not processed 0 ----------- times (seconds) ----------- run time 0.50 input time 0.08 binary_res time 0.00 hyper_res time 0.18 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.14 demod time 0.00 weigh time 0.02 for_sub time 0.08 unit_del time 0.00 post_process time 0.02 back_sub time 0.00 conflict time 0.00 factor time 0.00 FPA build time 0.02 IS build time 0.04 print_cl time 0.04 cl integrate time 0.00 window time 0.00 SHAR_EOF if test -f 'tandl27.desc' then echo shar: over-writing existing file "'tandl27.desc'" fi cat << \SHAR_EOF > 'tandl27.desc' problem-set/puzzles/truth_lies/tandl27.desc Created : 09/03/86 Revised : 07/18/88 Natural Language Description: Truthtellers and Liars Puzzle #27 There is an island with exactly two types of people--truthtellers who always tell the truth and liars who always lie. There are a group of three people, A, B, and C on the island. A stranger passes by and asks A, "How many truthtellers are among you ?" A answers indistinctly. So the stranger asks B, "what did A say?". B replies "A said that there is exactly one truthteller among us." Then C says, "Don't believe B; he is lying!" What are B and C. Versions: tandl27.ver1 : Declarative representation, using hyper-resolution. answer: B is a liar and C is a truth-teller. created by : Swaminathan and Pillai verified for ITP : 09/03/86 translated for OTTER by : K.R. verified for OTTER : 07/18/88 SHAR_EOF if test -f 'tandl27.ver1.clauses' then echo shar: over-writing existing file "'tandl27.ver1.clauses'" fi cat << \SHAR_EOF > 'tandl27.ver1.clauses' % problem-set/puzzles/truth_lies/tandl27.ver1.clauses % created : 07/14/88 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #27" using hyper- % resolution. % % Truthtellers and Liars Puzzle #27 % % There is an island with exactly two types of people--truthtellers % who always tell the truth and liars who always lie. % There are a group of three people, A, B, and C on the island. % A stranger passes by and asks A, "How many truthtellers are % among you ?" A answers indistinctly. So the stranger asks B, % "what did A say?". B replies "A said that there is exactly one % truthteller among us." Then C says, "Don't believe B; he is % lying!" What are B and C? % representation: % TRUE(atr(x)) | TRUE(liar(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y) . -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)). TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)). -P(x,y,z) | -TRUE(onett) | TRUE(atr(x)) | TRUE(atr(y)) | TRUE(atr(z)). -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(y)) | -TRUE(onett). -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(z)) | -TRUE(onett). -P(x,y,z) | -TRUE(atr(y)) | -TRUE(atr(z)) | -TRUE(onett). -P(x,y,z) | TRUE(onett) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(atr(z)). -P(x,y,z) | TRUE(onett) | -TRUE(atr(y)) | TRUE(atr(x)) | TRUE(atr(z)). -P(x,y,z) | TRUE(onett) | -TRUE(atr(z)) | TRUE(atr(y)) | TRUE(atr(x)). P(a,b,c). TRUE(Said(a,garbage)). TRUE(Said(b,Said(a,onett))). TRUE(Said(c,liar(b))). SHAR_EOF if test -f 'tandl27.ver1.in' then echo shar: over-writing existing file "'tandl27.ver1.in'" fi cat << \SHAR_EOF > 'tandl27.ver1.in' % problem-set/puzzles/truth_lies/tandl27.ver1.in % created : 09/03/86 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #27" using hyper- % resolution. % % Truthtellers and Liars Puzzle #27 % % There is an island with exactly two types of people--truthtellers % who always tell the truth and liars who always lie. % There are a group of three people, A, B, and C on the island. % A stranger passes by and asks A, "How many truthtellers are % among you ?" A answers indistinctly. So the stranger asks B, % "what did A say?". B replies "A said that there is exactly one % truthteller among us." Then C says, "Don't believe B; he is % lying!" What are B and C? % representation: % % Declarative version set(hyper_res). list(axioms). TRUE(atr(x)) | TRUE(liar(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y) . -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)). TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)). -P(x,y,z) | -TRUE(onett) | TRUE(atr(x)) | TRUE(atr(y)) | TRUE(atr(z)). -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(y)) | -TRUE(onett). -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(z)) | -TRUE(onett). -P(x,y,z) | -TRUE(atr(y)) | -TRUE(atr(z)) | -TRUE(onett). -P(x,y,z) | TRUE(onett) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(atr(z)). -P(x,y,z) | TRUE(onett) | -TRUE(atr(y)) | TRUE(atr(x)) | TRUE(atr(z)). -P(x,y,z) | TRUE(onett) | -TRUE(atr(z)) | TRUE(atr(y)) | TRUE(atr(x)). end_of_list. list(sos). P(a,b,c). TRUE(Said(a,garbage)). TRUE(Said(b,Said(a,onett))). TRUE(Said(c,liar(b))). end_of_list. SHAR_EOF if test -f 'tandl27.ver1.out' then echo shar: over-writing existing file "'tandl27.ver1.out'" fi cat << \SHAR_EOF > 'tandl27.ver1.out' problem-set/puzzles/truth_lies/tandl27.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 TRUE(atr(x)) | TRUE(liar(x)). 2 -TRUE(atr(x)) | -TRUE(liar(x)). 3 -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y). 4 -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y). 5 -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)). 6 TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)). 7 -P(x,y,z) | -TRUE(onett) | TRUE(atr(x)) | TRUE(atr(y)) | TRUE(atr(z)). 8 -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(y)) | -TRUE(onett). 9 -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(z)) | -TRUE(onett). 10 -P(x,y,z) | -TRUE(atr(y)) | -TRUE(atr(z)) | -TRUE(onett). 11 -P(x,y,z) | TRUE(onett) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(atr(z)). 12 -P(x,y,z) | TRUE(onett) | -TRUE(atr(y)) | TRUE(atr(x)) | TRUE(atr(z)). 13 -P(x,y,z) | TRUE(onett) | -TRUE(atr(z)) | TRUE(atr(y)) | TRUE(atr(x)). end_of_list. list(sos). 14 P(a,b,c). 15 TRUE(Said(a,garbage)). 16 TRUE(Said(b,Said(a,onett))). 17 TRUE(Said(c,liar(b))). end_of_list. new given clause: 14 P(a,b,c). ** KEPT: 18 (14,13,1) TRUE(onett) | TRUE(atr(b)) | TRUE(atr(a)) | TRUE(liar(c)). ** KEPT: 19 (14,12,1) TRUE(onett) | TRUE(atr(a)) | TRUE(atr(c)) | TRUE(liar(b)). ** KEPT: 20 (14,11,1) TRUE(onett) | TRUE(atr(b)) | TRUE(atr(c)) | TRUE(liar(a)). new given clause: 15 TRUE(Said(a,garbage)). ** KEPT: 21 (15,6) TRUE(garbage) | TRUE(liar(a)). new given clause: 17 TRUE(Said(c,liar(b))). ** KEPT: 22 (17,6) TRUE(liar(b)) | TRUE(liar(c)). ** KEPT: 23 (17,5,1) TRUE(atr(c)) | TRUE(atr(b)). 23 back subsumes: 20 (14,11,1) TRUE(onett) | TRUE(atr(b)) | TRUE(atr(c)) | TRUE(liar(a)). new given clause: 21 (15,6) TRUE(garbage) | TRUE(liar(a)). new given clause: 16 TRUE(Said(b,Said(a,onett))). ** KEPT: 24 (16,6) TRUE(Said(a,onett)) | TRUE(liar(b)). new given clause: 22 (17,6) TRUE(liar(b)) | TRUE(liar(c)). new given clause: 23 (17,5,1) TRUE(atr(c)) | TRUE(atr(b)). ** KEPT: 25 (23,13,14) TRUE(atr(b)) | TRUE(onett) | TRUE(atr(a)). ** KEPT: 26 (23,12,14) TRUE(atr(c)) | TRUE(onett) | TRUE(atr(a)). ** KEPT: 27 (23,3,16) TRUE(atr(c)) | TRUE(Said(a,onett)). 25 back subsumes: 18 (14,13,1) TRUE(onett) | TRUE(atr(b)) | TRUE(atr(a)) | TRUE(liar(c)). 26 back subsumes: 19 (14,12,1) TRUE(onett) | TRUE(atr(a)) | TRUE(atr(c)) | TRUE(liar(b)). new given clause: 24 (16,6) TRUE(Said(a,onett)) | TRUE(liar(b)). ** KEPT: 28 (24,6) TRUE(liar(b)) | TRUE(onett) | TRUE(liar(a)). new given clause: 27 (23,3,16) TRUE(atr(c)) | TRUE(Said(a,onett)). ** KEPT: 29 (27,6) TRUE(atr(c)) | TRUE(onett) | TRUE(liar(a)). new given clause: 25 (23,13,14) TRUE(atr(b)) | TRUE(onett) | TRUE(atr(a)). ** KEPT: 30 (25,3,16) TRUE(onett) | TRUE(atr(a)) | TRUE(Said(a,onett)). ** KEPT: 31 (25,2,22) TRUE(onett) | TRUE(atr(a)) | TRUE(liar(c)). ** KEPT: 32 (25,3,15) TRUE(atr(b)) | TRUE(onett) | TRUE(garbage). new given clause: 32 (25,3,15) TRUE(atr(b)) | TRUE(onett) | TRUE(garbage). ** KEPT: 33 (32,3,16) TRUE(onett) | TRUE(garbage) | TRUE(Said(a,onett)). ** KEPT: 34 (32,2,22) TRUE(onett) | TRUE(garbage) | TRUE(liar(c)). new given clause: 34 (32,2,22) TRUE(onett) | TRUE(garbage) | TRUE(liar(c)). new given clause: 26 (23,12,14) TRUE(atr(c)) | TRUE(onett) | TRUE(atr(a)). ** KEPT: 35 (26,3,17) TRUE(onett) | TRUE(atr(a)) | TRUE(liar(b)). ** KEPT: 36 (26,2,34) TRUE(onett) | TRUE(atr(a)) | TRUE(garbage). ** KEPT: 37 (26,5,27) TRUE(atr(c)) | TRUE(atr(a)). ** KEPT: 38 (26,3,27) TRUE(atr(c)) | TRUE(onett). 37 back subsumes: 26 (23,12,14) TRUE(atr(c)) | TRUE(onett) | TRUE(atr(a)). 38 back subsumes: 29 (27,6) TRUE(atr(c)) | TRUE(onett) | TRUE(liar(a)). new given clause: 38 (26,3,27) TRUE(atr(c)) | TRUE(onett). ** KEPT: 39 (38,3,17) TRUE(onett) | TRUE(liar(b)). ** KEPT: 40 (38,2,34) TRUE(onett) | TRUE(garbage). ** KEPT: 41 (38,8,14,1,23) TRUE(atr(c)) | TRUE(liar(a)). ** KEPT: 42 (38,4,21,27) TRUE(atr(c)) | TRUE(garbage). 39 back subsumes: 35 (26,3,17) TRUE(onett) | TRUE(atr(a)) | TRUE(liar(b)). 39 back subsumes: 28 (24,6) TRUE(liar(b)) | TRUE(onett) | TRUE(liar(a)). 40 back subsumes: 36 (26,2,34) TRUE(onett) | TRUE(atr(a)) | TRUE(garbage). 40 back subsumes: 34 (32,2,22) TRUE(onett) | TRUE(garbage) | TRUE(liar(c)). 40 back subsumes: 33 (32,3,16) TRUE(onett) | TRUE(garbage) | TRUE(Said(a,onett)). 40 back subsumes: 32 (25,3,15) TRUE(atr(b)) | TRUE(onett) | TRUE(garbage). new given clause: 40 (38,2,34) TRUE(onett) | TRUE(garbage). ** KEPT: 43 (40,5,24) TRUE(garbage) | TRUE(atr(a)) | TRUE(liar(b)). ** KEPT: 44 (40,4,21,24) TRUE(garbage) | TRUE(liar(b)). ** KEPT: 45 (40,5,15) TRUE(onett) | TRUE(atr(a)). 44 back subsumes: 43 (40,5,24) TRUE(garbage) | TRUE(atr(a)) | TRUE(liar(b)). 45 back subsumes: 31 (25,2,22) TRUE(onett) | TRUE(atr(a)) | TRUE(liar(c)). 45 back subsumes: 30 (25,3,16) TRUE(onett) | TRUE(atr(a)) | TRUE(Said(a,onett)). 45 back subsumes: 25 (23,13,14) TRUE(atr(b)) | TRUE(onett) | TRUE(atr(a)). new given clause: 39 (38,3,17) TRUE(onett) | TRUE(liar(b)). ** KEPT: 46 (39,8,14,1,1) TRUE(liar(b)) | TRUE(liar(a)). ** KEPT: 47 (39,5,24) TRUE(liar(b)) | TRUE(atr(a)). new given clause: 42 (38,4,21,27) TRUE(atr(c)) | TRUE(garbage). new given clause: 44 (40,4,21,24) TRUE(garbage) | TRUE(liar(b)). new given clause: 45 (40,5,15) TRUE(onett) | TRUE(atr(a)). new given clause: 37 (26,5,27) TRUE(atr(c)) | TRUE(atr(a)). ** KEPT: 48 (37,8,14,23,39) TRUE(atr(c)) | TRUE(liar(b)). ** KEPT: 49 (37,8,14,23,38) TRUE(atr(c)). 49 back subsumes: 48 (37,8,14,23,39) TRUE(atr(c)) | TRUE(liar(b)). 49 back subsumes: 42 (38,4,21,27) TRUE(atr(c)) | TRUE(garbage). 49 back subsumes: 41 (38,8,14,1,23) TRUE(atr(c)) | TRUE(liar(a)). 49 back subsumes: 38 (26,3,27) TRUE(atr(c)) | TRUE(onett). 49 back subsumes: 37 (26,5,27) TRUE(atr(c)) | TRUE(atr(a)). 49 back subsumes: 27 (23,3,16) TRUE(atr(c)) | TRUE(Said(a,onett)). 49 back subsumes: 23 (17,5,1) TRUE(atr(c)) | TRUE(atr(b)). new given clause: 49 (37,8,14,23,38) TRUE(atr(c)). ** KEPT: 50 (49,10,14,1,39) TRUE(liar(b)). 50 back subsumes: 47 (39,5,24) TRUE(liar(b)) | TRUE(atr(a)). 50 back subsumes: 46 (39,8,14,1,1) TRUE(liar(b)) | TRUE(liar(a)). 50 back subsumes: 44 (40,4,21,24) TRUE(garbage) | TRUE(liar(b)). 50 back subsumes: 39 (38,3,17) TRUE(onett) | TRUE(liar(b)). 50 back subsumes: 24 (16,6) TRUE(Said(a,onett)) | TRUE(liar(b)). 50 back subsumes: 22 (17,6) TRUE(liar(b)) | TRUE(liar(c)). new given clause: 50 (49,10,14,1,39) TRUE(liar(b)). ------------ END OF SEARCH ------------ sos empty. --------------- 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 17 clauses given 22 clauses generated 615 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 582 (clauses subsumed by sos) 129 unit deletions 0 clauses kept 33 empty clauses 0 factors generated 0 clauses back subsumed 28 clauses not processed 0 ----------- times (seconds) ----------- run time 3.96 input time 0.20 binary_res time 0.00 hyper_res time 1.78 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 1.64 demod time 0.00 weigh time 0.02 for_sub time 1.10 unit_del time 0.00 post_process time 0.18 back_sub time 0.10 conflict time 0.00 factor time 0.00 FPA build time 0.04 IS build time 0.02 print_cl time 0.28 cl integrate time 0.04 window time 0.00 SHAR_EOF if test -f 'tandl31.desc' then echo shar: over-writing existing file "'tandl31.desc'" fi cat << \SHAR_EOF > 'tandl31.desc' problem-set/puzzles/truth_lies/tandl31.desc created : 09/03/86 revised : 07/18/88 Natural Language Description: Truthtellers and Liars Puzzle #31 There is an island with exactly two types of people--truthtellers who always tell the truth and liars who always lie. There are a group of three people, A, B, and C on the island. A and B make the following statements. A: All of us are liars; B: Exactly one of us is a truthteller. What are A, B, and C? Versions: tandl31.ver1 : Declarative representation, using hyper-resolution. answer: A is a liar, B is a truthteller, and C is a liar. created by : Swaminathan verified for ITP : 09/03/86 translated for OTTER by : K.R. verified for OTTER : 07/18/88 SHAR_EOF if test -f 'tandl31.ver1.clauses' then echo shar: over-writing existing file "'tandl31.ver1.clauses'" fi cat << \SHAR_EOF > 'tandl31.ver1.clauses' % problem-set/puzzles/truth_lies/tandl31.ver1.clauses % created : 07/14/88 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #31" using hyper- % resolution. % % Truthtellers and Liars Puzzle #31 % % There is an island with exactly two types of people--truthtellers who % always tell the truth and liars who always lie. % There are a group of three people, A, B, and C on the island. % A and B make the following statements. A: All of us are liars; B: % Exactly one of us is a truthteller. What are A, B, and C ? % representation: % % declare_predicate(1,P). % declare_predicate(3,PER). % declare_functions(1,[atr,liar]). % declare_function(2,asaid). % declare_variables([x,y,z]). % declare_constants([a,b,c,oneofus,allofus]). % % Meanings of significant predicates and functions % P(x) means "x is true" % PER(x,y,z) means x,y, and z are persons under consideration % in this puzzle . % Said(x,y) means "x made the statement y " % atr(x) means "x is a truthteller" % liar(x) means "x is a liar" % x is either a truthteller or a liar P(atr(x)) | P(liar(x)). % If x is a truthteller, he cannot be a liar -P(atr(x)) | -P(liar(x)). % If x is a truthteller and he says that one of us is a truthteller % then obviously, he is the only one % it it important to define the meaning of "exactly one of us" % The following clauses define this term and the negation of the same -P(Said(x,oneofus)) |-PER(x,y,z) |-P(atr(x))| -P(atr(y)) | -P(atr(z)) . -P(oneofus) |-PER(x,y,z) |P(atr(x))| P(atr(y)) | P(atr(z)) . -P(oneofus) |-PER(x,y,z) |-P(atr(y))| -P(atr(x)) | -P(atr(z)) . -P(oneofus) |-PER(x,y,z) |-P(liar(x)) |-P(atr(y)) | P(liar(z)). P(oneofus) |-PER(x,y,z) |-P(liar(x)) |-P(atr(y)) | P(atr(z)). P(oneofus) |-PER(x,y,z) |-P(liar(x)) |-P(liar(y)) | P(liar(z)). % If x says that 'all of us' are liars then, all the persons. % indicated by PER may be liars. -P(Said(x,allofus)) |-PER(x,y,z) |-P(atr(x)). P(allofus) | -PER(x,y,z) | P(atr(x)) | P(atr(y)) |P(atr(z)). % A truthteller always says the truth. -P(atr(x)) | -P(Said(x,y)) | P(y). -P(y) |-P(Said(x,y)) |P(atr(x)). % A liar always lies. -P(liar(x)) | -P(Said(x,y)) | -P(y). P(y) |-P(Said(x,y)) | P(liar(x)). PER(b,c,a). PER(a,c,b). PER(c,b,a). P(Said(a,allofus)). P(Said(b,oneofus)). SHAR_EOF if test -f 'tandl31.ver1.in' then echo shar: over-writing existing file "'tandl31.ver1.in'" fi cat << \SHAR_EOF > 'tandl31.ver1.in' % problem-set/puzzles/truth_lies/tandl31.ver1.in % created : 09/03/86 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #31" using hyper- % resolution. % % Truthtellers and Liars Puzzle #31 % % There is an island with exactly two types of people--truthtellers who % always tell the truth and liars who always lie. % There are a group of three people, A, B, and C on the island. % A and B make the following statements. A: All of us are liars; B: % Exactly one of us is a truthteller. What are A, B, and C ? % representation: % % declare_predicate(1,P). % declare_predicate(3,PER). % declare_functions(1,[atr,liar]). % declare_function(2,asaid). % declare_variables([x,y,z]). % declare_constants([a,b,c,oneofus,allofus]). % % Meanings of significant predicates and functions % P(x) means "x is true" % PER(x,y,z) means x,y, and z are persons under consideration % in this puzzle . % Said(x,y) means "x made the statement y " % atr(x) means "x is a truthteller" % liar(x) means "x is a liar" set(hyper_res). list(axioms). % x is either a truthteller or a liar P(atr(x)) | P(liar(x)). % If x is a truthteller, he cannot be a liar -P(atr(x)) | -P(liar(x)). % If x is a truthteller and he says that one of us is a truthteller % then obviously, he is the only one % it it important to define the meaning of "exactly one of us" % The following clauses define this term and the negation of the same -P(Said(x,oneofus)) |-PER(x,y,z) |-P(atr(x))| -P(atr(y)) | -P(atr(z)) . -P(oneofus) |-PER(x,y,z) |P(atr(x))| P(atr(y)) | P(atr(z)) . -P(oneofus) |-PER(x,y,z) |-P(atr(y))| -P(atr(x)) | -P(atr(z)) . -P(oneofus) |-PER(x,y,z) |-P(liar(x)) |-P(atr(y)) | P(liar(z)). P(oneofus) |-PER(x,y,z) |-P(liar(x)) |-P(atr(y)) | P(atr(z)). P(oneofus) |-PER(x,y,z) |-P(liar(x)) |-P(liar(y)) | P(liar(z)). % If x says that 'all of us' are liars then, all the persons. % indicated by PER may be liars. -P(Said(x,allofus)) |-PER(x,y,z) |-P(atr(x)). P(allofus) | -PER(x,y,z) | P(atr(x)) | P(atr(y)) |P(atr(z)). % A truthteller always says the truth. -P(atr(x)) | -P(Said(x,y)) | P(y). -P(y) |-P(Said(x,y)) |P(atr(x)). % A liar always lies. -P(liar(x)) | -P(Said(x,y)) | -P(y). P(y) |-P(Said(x,y)) | P(liar(x)). end_of_list. list(sos). PER(b,c,a). PER(a,c,b). PER(c,b,a). P(Said(a,allofus)). P(Said(b,oneofus)). end_of_list. SHAR_EOF if test -f 'tandl31.ver1.out' then echo shar: over-writing existing file "'tandl31.ver1.out'" fi cat << \SHAR_EOF > 'tandl31.ver1.out' problem-set/puzzles/truth_lies/tandl31.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 P(atr(x)) | P(liar(x)). 2 -P(atr(x)) | -P(liar(x)). 3 -P(Said(x,oneofus)) | -PER(x,y,z) | -P(atr(x)) | -P(atr(y)) | -P(atr(z)). 4 -P(oneofus) | -PER(x,y,z) | P(atr(x)) | P(atr(y)) | P(atr(z)). 5 -P(oneofus) | -PER(x,y,z) | -P(atr(y)) | -P(atr(x)) | -P(atr(z)). 6 -P(oneofus) | -PER(x,y,z) | -P(liar(x)) | -P(atr(y)) | P(liar(z)). 7 P(oneofus) | -PER(x,y,z) | -P(liar(x)) | -P(atr(y)) | P(atr(z)). 8 P(oneofus) | -PER(x,y,z) | -P(liar(x)) | -P(liar(y)) | P(liar(z)). 9 -P(Said(x,allofus)) | -PER(x,y,z) | -P(atr(x)). 10 P(allofus) | -PER(x,y,z) | P(atr(x)) | P(atr(y)) | P(atr(z)). 11 -P(atr(x)) | -P(Said(x,y)) | P(y). 12 -P(y) | -P(Said(x,y)) | P(atr(x)). 13 -P(liar(x)) | -P(Said(x,y)) | -P(y). 14 P(y) | -P(Said(x,y)) | P(liar(x)). end_of_list. list(sos). 15 PER(b,c,a). 16 PER(a,c,b). 17 PER(c,b,a). 18 P(Said(a,allofus)). 19 P(Said(b,oneofus)). end_of_list. new given clause: 15 PER(b,c,a). ** KEPT: 20 (15,10) P(allofus) | P(atr(b)) | P(atr(c)) | P(atr(a)). ** KEPT: 21 (15,8,1,1) P(oneofus) | P(liar(a)) | P(atr(b)) | P(atr(c)). ** KEPT: 22 (15,7,1,1) P(oneofus) | P(atr(a)) | P(atr(b)) | P(liar(c)). new given clause: 16 PER(a,c,b). ** KEPT: 23 (16,8,1,1) P(oneofus) | P(liar(b)) | P(atr(a)) | P(atr(c)). new given clause: 17 PER(c,b,a). new given clause: 18 P(Said(a,allofus)). ** KEPT: 24 (18,14) P(allofus) | P(liar(a)). ** KEPT: 25 (18,9,16,1) P(liar(a)). 25 back subsumes: 24 (18,14) P(allofus) | P(liar(a)). 25 back subsumes: 21 (15,8,1,1) P(oneofus) | P(liar(a)) | P(atr(b)) | P(atr(c)). new given clause: 25 (18,9,16,1) P(liar(a)). ** KEPT: 26 (25,8,16,1) P(oneofus) | P(liar(b)) | P(atr(c)). ** KEPT: 27 (25,7,16,1) P(oneofus) | P(atr(b)) | P(liar(c)). 26 back subsumes: 23 (16,8,1,1) P(oneofus) | P(liar(b)) | P(atr(a)) | P(atr(c)). 27 back subsumes: 22 (15,7,1,1) P(oneofus) | P(atr(a)) | P(atr(b)) | P(liar(c)). new given clause: 19 P(Said(b,oneofus)). ** KEPT: 28 (19,14) P(oneofus) | P(liar(b)). 28 back subsumes: 26 (25,8,16,1) P(oneofus) | P(liar(b)) | P(atr(c)). new given clause: 28 (19,14) P(oneofus) | P(liar(b)). ** KEPT: 29 (28,6,16,25,1) P(liar(b)) | P(liar(c)). ** KEPT: 30 (28,7,15,1) P(oneofus) | P(atr(a)) | P(liar(c)). new given clause: 29 (28,6,16,25,1) P(liar(b)) | P(liar(c)). new given clause: 27 (25,7,16,1) P(oneofus) | P(atr(b)) | P(liar(c)). ** KEPT: 31 (27,13,29,19) P(atr(b)) | P(liar(c)). ** KEPT: 32 (27,11,19) P(oneofus) | P(liar(c)). 31 back subsumes: 27 (25,7,16,1) P(oneofus) | P(atr(b)) | P(liar(c)). 32 back subsumes: 30 (28,7,15,1) P(oneofus) | P(atr(a)) | P(liar(c)). new given clause: 32 (27,11,19) P(oneofus) | P(liar(c)). ** KEPT: 33 (32,13,29,19) P(liar(c)). 33 back subsumes: 32 (27,11,19) P(oneofus) | P(liar(c)). 33 back subsumes: 31 (27,13,29,19) P(atr(b)) | P(liar(c)). 33 back subsumes: 29 (28,6,16,25,1) P(liar(b)) | P(liar(c)). new given clause: 33 (32,13,29,19) P(liar(c)). new given clause: 20 (15,10) P(allofus) | P(atr(b)) | P(atr(c)) | P(atr(a)). ** KEPT: 34 (20,13,25,18) P(atr(b)) | P(atr(c)) | P(atr(a)). ** KEPT: 35 (20,11,19) P(allofus) | P(atr(c)) | P(atr(a)) | P(oneofus). ** KEPT: 36 (20,7,16,25) P(allofus) | P(atr(b)) | P(atr(a)) | P(oneofus). ** KEPT: 37 (20,2,33) P(allofus) | P(atr(b)) | P(atr(a)). ** KEPT: 38 (20,11,18) P(allofus) | P(atr(b)) | P(atr(c)). 34 back subsumes: 20 (15,10) P(allofus) | P(atr(b)) | P(atr(c)) | P(atr(a)). 37 back subsumes: 36 (20,7,16,25) P(allofus) | P(atr(b)) | P(atr(a)) | P(oneofus). new given clause: 37 (20,2,33) P(allofus) | P(atr(b)) | P(atr(a)). ** KEPT: 39 (37,13,25,18) P(atr(b)) | P(atr(a)). ** KEPT: 40 (37,11,19) P(allofus) | P(atr(a)) | P(oneofus). ** KEPT: 41 (37,11,18) P(allofus) | P(atr(b)). 39 back subsumes: 37 (20,2,33) P(allofus) | P(atr(b)) | P(atr(a)). 39 back subsumes: 34 (20,13,25,18) P(atr(b)) | P(atr(c)) | P(atr(a)). 40 back subsumes: 35 (20,11,19) P(allofus) | P(atr(c)) | P(atr(a)) | P(oneofus). 41 back subsumes: 38 (20,11,18) P(allofus) | P(atr(b)) | P(atr(c)). new given clause: 41 (37,11,18) P(allofus) | P(atr(b)). ** KEPT: 42 (41,13,25,18) P(atr(b)). ** KEPT: 43 (41,11,19) P(allofus) | P(oneofus). 42 back subsumes: 41 (37,11,18) P(allofus) | P(atr(b)). 42 back subsumes: 39 (37,13,25,18) P(atr(b)) | P(atr(a)). 43 back subsumes: 40 (37,11,19) P(allofus) | P(atr(a)) | P(oneofus). new given clause: 42 (41,13,25,18) P(atr(b)). ** KEPT: 44 (42,11,19) P(oneofus). 44 back subsumes: 43 (41,11,19) P(allofus) | P(oneofus). 44 back subsumes: 28 (19,14) P(oneofus) | P(liar(b)). 44 back subsumes: 8 P(oneofus) | -PER(x,y,z) | -P(liar(x)) | -P(liar(y)) | P(liar(z)). 44 back subsumes: 7 P(oneofus) | -PER(x,y,z) | -P(liar(x)) | -P(atr(y)) | P(atr(z)). new given clause: 44 (42,11,19) P(oneofus). ------------ END OF SEARCH ------------ sos empty. --------------- 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 19 clauses given 16 clauses generated 300 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 275 (clauses subsumed by sos) 119 unit deletions 0 clauses kept 25 empty clauses 0 factors generated 0 clauses back subsumed 23 clauses not processed 0 ----------- times (seconds) ----------- run time 3.06 input time 0.18 binary_res time 0.00 hyper_res time 1.70 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.88 demod time 0.00 weigh time 0.00 for_sub time 0.64 unit_del time 0.00 post_process time 0.16 back_sub time 0.02 conflict time 0.04 factor time 0.00 FPA build time 0.02 IS build time 0.02 print_cl time 0.10 cl integrate time 0.02 window time 0.00 SHAR_EOF if test -f 'tandl35.desc' then echo shar: over-writing existing file "'tandl35.desc'" fi cat << \SHAR_EOF > 'tandl35.desc' problem-set/puzzles/truth_lies/tandl35.desc created : 09/03/86 revised : 07/18/88 Natural Language Description: Truthtellers and Liars Puzzle #35 There is an island with exactly two types of people-- truthtellers who always tell the truth and liars who always lie. There are a group of three people, A, B, and C on the island. A and B make the following statements. A: "B and C are the same type". Someone asks "Are A and B of the same type ? " What does C answer ? Versions: tandl35.ver1 : Declarative represention, using UR-resolution. answer: "yes" created by : Swaminathan verified for ITP : 09/03/86 translated for OTTER by : K.R. verified for OTTER : 07/18/88 SHAR_EOF if test -f 'tandl35.ver1.clauses' then echo shar: over-writing existing file "'tandl35.ver1.clauses'" fi cat << \SHAR_EOF > 'tandl35.ver1.clauses' % problem-set/puzzles/truth_lies/tandl35.ver1.clauses % created : 07/18/88 % revised : 07/18/88 % description: % % This run solves "Truthtellers and Liars Puzzle #31" using hyper- % resolution. % % Truthtellers and Liars Puzzle #31 % % There is an island with exactly two types of people--truthtellers who % always tell the truth and liars who always lie. % There are a group of three people, A, B, and C on the island. % A and B make the following statements. A: "B and C are the same type". % Someone asks "Are A and B of the same type ? " What does C answer ? % representation: % % declare_predicate(1,P). % declare_predicate(3,PER). % declare_functions(1,[atr,liar]). % declare_function(2,asaid). % declare_variables([x,y,z]). % declare_constants([a,b,c,oneofus,allofus]). % % Meanings of significant predicates and functions % P(x) means "x is true" % PER(x,y,z) means x,y, and z are persons under consideration % in this puzzle % Said(x,y) means "x made the statement y " % atr(x) means "x is a truthteller" % liar(x) means "x is a liar" % x is either a truthteller or a liar P(atr(x)) | P(liar(x)). % If x is a truthteller, he cannot be a liar -P(atr(x)) | -P(liar(x)). % A truthteller always says the truth. -P(atr(x)) | -P(Said(x,y)) | P(y). -P(y) |-P(Said(x,y)) |P(atr(x)). % A liar always lies. -P(liar(x)) | -P(Said(x,y)) | -P(y). P(y) |-P(Said(x,y)) | P(liar(x)). % This is the definition of "2 persons being of the same type " -PERSON(x,y,z) | -P(liar(x)) |-P(liar(y)) | P(equatype(x,y)). -PERSON(x,y,z) | -P(atr(x)) |-P(atr(y)) | P(equatype(x,y)). -P(equatype(x,y)) | -P(atr(x)) | P(atr(y)) . -P(equatype(x,y)) | -P(liar(x)) | P(liar(y)) . -P(atr(x)) | P(equatype(x,y)) | P(liar(y)) . -P(liar(x)) | P(equatype(x,y)) | P(atr(y)) . -P(equatype(x,y)) | P(equatype(y,x)). % If one of the inhabitants are questioned, the answer is represented % as follows -Q(x,y) | -P(atr(x)) | -P(y) | Answer(Y) . -Q(x,y) | -P(atr(x)) | P(y) | Answer(N) . -Q(x,y) | -P(liar(x)) | -P(y) | Answer(N) . -Q(x,y) | -P(liar(x)) | P(y) | Answer(Y) . PERSON(b,c,a). PERSON(a,b,a). PERSON(a,c,b). PERSON(c,b,a). P(Said(a,equatype(b,c))). Q(c,equatype(a,b)). SHAR_EOF if test -f 'tandl35.ver1.in' then echo shar: over-writing existing file "'tandl35.ver1.in'" fi cat << \SHAR_EOF > 'tandl35.ver1.in' % problem-set/puzzles/truth_lies/tandl35.ver1.in % created : 09/03/86 % revised : 07/18/88 % description: % % This run solves "Truthtellers and Liars Puzzle #31" using hyper- % resolution. % % Truthtellers and Liars Puzzle #31 % % There is an island with exactly two types of people--truthtellers who % always tell the truth and liars who always lie. % There are a group of three people, A, B, and C on the island. % A and B make the following statements. A: "B and C are the same type". % Someone asks "Are A and B of the same type ? " What does C answer ? % representation: % % declare_predicate(1,P). % declare_predicate(3,PER). % declare_functions(1,[atr,liar]). % declare_function(2,asaid). % declare_variables([x,y,z]). % declare_constants([a,b,c,oneofus,allofus]). % % Meanings of significant predicates and functions % P(x) means "x is true" % PER(x,y,z) means x,y, and z are persons under consideration % in this puzzle % Said(x,y) means "x made the statement y " % atr(x) means "x is a truthteller" % liar(x) means "x is a liar" set(hyper_res). assign(max_given,40). list(axioms). % x is either a truthteller or a liar P(atr(x)) | P(liar(x)). % If x is a truthteller, he cannot be a liar -P(atr(x)) | -P(liar(x)). % A truthteller always says the truth. -P(atr(x)) | -P(Said(x,y)) | P(y). -P(y) |-P(Said(x,y)) |P(atr(x)). % A liar always lies. -P(liar(x)) | -P(Said(x,y)) | -P(y). P(y) |-P(Said(x,y)) | P(liar(x)). % This is the definition of "2 persons being of the same type " -PERSON(x,y,z) | -P(liar(x)) |-P(liar(y)) | P(equatype(x,y)). -PERSON(x,y,z) | -P(atr(x)) |-P(atr(y)) | P(equatype(x,y)). -P(equatype(x,y)) | -P(atr(x)) | P(atr(y)) . -P(equatype(x,y)) | -P(liar(x)) | P(liar(y)) . -P(atr(x)) | P(equatype(x,y)) | P(liar(y)) . -P(liar(x)) | P(equatype(x,y)) | P(atr(y)) . -P(equatype(x,y)) | P(equatype(y,x)). % If one of the inhabitants are questioned, the answer is represented % as follows -Q(x,y) | -P(atr(x)) | -P(y) | Answer(Y) . -Q(x,y) | -P(atr(x)) | P(y) | Answer(N) . -Q(x,y) | -P(liar(x)) | -P(y) | Answer(N) . -Q(x,y) | -P(liar(x)) | P(y) | Answer(Y) . end_of_list. list(sos). PERSON(b,c,a). PERSON(a,b,a). PERSON(a,c,b). PERSON(c,b,a). P(Said(a,equatype(b,c))). Q(c,equatype(a,b)). end_of_list. SHAR_EOF if test -f 'tandl35.ver1.out' then echo shar: over-writing existing file "'tandl35.ver1.out'" fi cat << \SHAR_EOF > 'tandl35.ver1.out' problem-set/puzzles/truth_lies/tandl35.ver1.out created : 07/18/88 revised : 07/18/88 OTTER version 0.91, 14 June 1988. set(hyper_res). assign(max_given,40). list(axioms). 1 P(atr(x)) | P(liar(x)). 2 -P(atr(x)) | -P(liar(x)). 3 -P(atr(x)) | -P(Said(x,y)) | P(y). 4 -P(y) | -P(Said(x,y)) | P(atr(x)). 5 -P(liar(x)) | -P(Said(x,y)) | -P(y). 6 P(y) | -P(Said(x,y)) | P(liar(x)). 7 -PERSON(x,y,z) | -P(liar(x)) | -P(liar(y)) | P(equatype(x,y)). 8 -PERSON(x,y,z) | -P(atr(x)) | -P(atr(y)) | P(equatype(x,y)). 9 -P(equatype(x,y)) | -P(atr(x)) | P(atr(y)). 10 -P(equatype(x,y)) | -P(liar(x)) | P(liar(y)). 11 -P(atr(x)) | P(equatype(x,y)) | P(liar(y)). 12 -P(liar(x)) | P(equatype(x,y)) | P(atr(y)). 13 -P(equatype(x,y)) | P(equatype(y,x)). 14 -Q(x,y) | -P(atr(x)) | -P(y) | Answer(Y). 15 -Q(x,y) | -P(atr(x)) | P(y) | Answer(N). 16 -Q(x,y) | -P(liar(x)) | -P(y) | Answer(N). 17 -Q(x,y) | -P(liar(x)) | P(y) | Answer(Y). end_of_list. list(sos). 18 PERSON(b,c,a). 19 PERSON(a,b,a). 20 PERSON(a,c,b). 21 PERSON(c,b,a). 22 P(Said(a,equatype(b,c))). 23 Q(c,equatype(a,b)). end_of_list. new given clause: 18 PERSON(b,c,a). ** KEPT: 24 (18,8,1,1) P(equatype(b,c)) | P(liar(b)) | P(liar(c)). ** KEPT: 25 (18,7,1,1) P(equatype(b,c)) | P(atr(b)) | P(atr(c)). new given clause: 19 PERSON(a,b,a). ** KEPT: 26 (19,8,1,1) P(equatype(a,b)) | P(liar(a)) | P(liar(b)). ** KEPT: 27 (19,7,1,1) P(equatype(a,b)) | P(atr(a)) | P(atr(b)). new given clause: 20 PERSON(a,c,b). ** KEPT: 28 (20,8,1,1) P(equatype(a,c)) | P(liar(a)) | P(liar(c)). ** KEPT: 29 (20,7,1,1) P(equatype(a,c)) | P(atr(a)) | P(atr(c)). new given clause: 21 PERSON(c,b,a). ** KEPT: 30 (21,8,1,1) P(equatype(c,b)) | P(liar(c)) | P(liar(b)). ** KEPT: 31 (21,7,1,1) P(equatype(c,b)) | P(atr(c)) | P(atr(b)). new given clause: 23 Q(c,equatype(a,b)). ** KEPT: 32 (23,17,1) P(equatype(a,b)) | Answer(Y) | P(atr(c)). ** KEPT: 33 (23,15,1) P(equatype(a,b)) | Answer(N) | P(liar(c)). new given clause: 22 P(Said(a,equatype(b,c))). ** KEPT: 34 (22,6) P(equatype(b,c)) | P(liar(a)). new given clause: 34 (22,6) P(equatype(b,c)) | P(liar(a)). ** KEPT: 35 (34,13) P(liar(a)) | P(equatype(c,b)). ** KEPT: 36 (34,10,1) P(liar(a)) | P(liar(c)) | P(atr(b)). ** KEPT: 37 (34,9,1) P(liar(a)) | P(atr(c)) | P(liar(b)). ** KEPT: 38 (34,12) P(equatype(b,c)) | P(equatype(a,x)) | P(atr(x)). new given clause: 35 (34,13) P(liar(a)) | P(equatype(c,b)). ** KEPT: 39 (35,12) P(equatype(c,b)) | P(equatype(a,x)) | P(atr(x)). new given clause: 32 (23,17,1) P(equatype(a,b)) | Answer(Y) | P(atr(c)). ** KEPT: 40 (32,16,23,1) Answer(Y) | P(atr(c)) | Answer(N). ** KEPT: 41 (32,13) Answer(Y) | P(atr(c)) | P(equatype(b,a)). ** KEPT: 42 (32,10,35) Answer(Y) | P(atr(c)) | P(liar(b)) | P(equatype(c,b)). ** KEPT: 43 (32,10,34) Answer(Y) | P(atr(c)) | P(liar(b)) | P(equatype(b,c)). ** KEPT: 44 (32,10,1) Answer(Y) | P(atr(c)) | P(liar(b)) | P(atr(a)). ** KEPT: 45 (32,9,1) Answer(Y) | P(atr(c)) | P(atr(b)) | P(liar(a)). ** KEPT: 46 (32,15,23) P(equatype(a,b)) | Answer(Y) | Answer(N). ** KEPT: 47 (32,11) P(equatype(a,b)) | Answer(Y) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 48 (32,9,35) P(equatype(a,b)) | Answer(Y) | P(atr(b)) | P(liar(a)). ** KEPT: 49 (32,8,20,1) P(equatype(a,b)) | Answer(Y) | P(equatype(a,c)) | P(liar(a)). ** KEPT: 50 (32,8,18,1) P(equatype(a,b)) | Answer(Y) | P(equatype(b,c)) | P(liar(b)). new given clause: 40 (32,16,23,1) Answer(Y) | P(atr(c)) | Answer(N). ** KEPT: 51 (40,11) Answer(Y) | Answer(N) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 52 (40,9,35) Answer(Y) | Answer(N) | P(atr(b)) | P(liar(a)). ** KEPT: 53 (40,8,20,1) Answer(Y) | Answer(N) | P(equatype(a,c)) | P(liar(a)). ** KEPT: 54 (40,8,18,1) Answer(Y) | Answer(N) | P(equatype(b,c)) | P(liar(b)). new given clause: 46 (32,15,23) P(equatype(a,b)) | Answer(Y) | Answer(N). ** KEPT: 55 (46,14,23,40) Answer(Y) | Answer(N). 55 back subsumes: 54 (40,8,18,1) Answer(Y) | Answer(N) | P(equatype(b,c)) | P(liar(b)). 55 back subsumes: 53 (40,8,20,1) Answer(Y) | Answer(N) | P(equatype(a,c)) | P(liar(a)). 55 back subsumes: 52 (40,9,35) Answer(Y) | Answer(N) | P(atr(b)) | P(liar(a)). 55 back subsumes: 51 (40,11) Answer(Y) | Answer(N) | P(equatype(c,x)) | P(liar(x)). 55 back subsumes: 46 (32,15,23) P(equatype(a,b)) | Answer(Y) | Answer(N). 55 back subsumes: 40 (32,16,23,1) Answer(Y) | P(atr(c)) | Answer(N). new given clause: 55 (46,14,23,40) Answer(Y) | Answer(N). new given clause: 33 (23,15,1) P(equatype(a,b)) | Answer(N) | P(liar(c)). ** KEPT: 56 (33,13) Answer(N) | P(liar(c)) | P(equatype(b,a)). ** KEPT: 57 (33,10,1) Answer(N) | P(liar(c)) | P(liar(b)) | P(atr(a)). ** KEPT: 58 (33,12) P(equatype(a,b)) | Answer(N) | P(equatype(c,x)) | P(atr(x)). ** KEPT: 59 (33,7,20,35) P(equatype(a,b)) | Answer(N) | P(equatype(a,c)) | P(equatype(c,b)). ** KEPT: 60 (33,7,20,34) P(equatype(a,b)) | Answer(N) | P(equatype(a,c)) | P(equatype(b,c)). ** KEPT: 61 (33,7,20,1) P(equatype(a,b)) | Answer(N) | P(equatype(a,c)) | P(atr(a)). new given clause: 36 (34,10,1) P(liar(a)) | P(liar(c)) | P(atr(b)). ** KEPT: 62 (36,12) P(liar(c)) | P(atr(b)) | P(equatype(a,x)) | P(atr(x)). ** KEPT: 63 (36,12) P(liar(a)) | P(atr(b)) | P(equatype(c,x)) | P(atr(x)). ** KEPT: 64 (36,11) P(liar(a)) | P(liar(c)) | P(equatype(b,x)) | P(liar(x)). ** KEPT: 65 (36,8,19,1) P(liar(a)) | P(liar(c)) | P(equatype(a,b)). new given clause: 37 (34,9,1) P(liar(a)) | P(atr(c)) | P(liar(b)). ** KEPT: 66 (37,12) P(atr(c)) | P(liar(b)) | P(equatype(a,x)) | P(atr(x)). ** KEPT: 67 (37,10,32) P(atr(c)) | P(liar(b)) | Answer(Y). ** KEPT: 68 (37,11) P(liar(a)) | P(liar(b)) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 69 (37,8,20,1) P(liar(a)) | P(liar(b)) | P(equatype(a,c)). ** KEPT: 70 (37,12) P(liar(a)) | P(atr(c)) | P(equatype(b,x)) | P(atr(x)). 67 back subsumes: 44 (32,10,1) Answer(Y) | P(atr(c)) | P(liar(b)) | P(atr(a)). 67 back subsumes: 43 (32,10,34) Answer(Y) | P(atr(c)) | P(liar(b)) | P(equatype(b,c)). 67 back subsumes: 42 (32,10,35) Answer(Y) | P(atr(c)) | P(liar(b)) | P(equatype(c,b)). new given clause: 67 (37,10,32) P(atr(c)) | P(liar(b)) | Answer(Y). ** KEPT: 71 (67,11) P(liar(b)) | Answer(Y) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 72 (67,8,18,1) P(liar(b)) | Answer(Y) | P(equatype(b,c)). ** KEPT: 73 (67,12) P(atr(c)) | Answer(Y) | P(equatype(b,x)) | P(atr(x)). ** KEPT: 74 (67,7,21,1) P(atr(c)) | Answer(Y) | P(equatype(c,b)). 72 back subsumes: 50 (32,8,18,1) P(equatype(a,b)) | Answer(Y) | P(equatype(b,c)) | P(liar(b)). new given clause: 41 (32,13) Answer(Y) | P(atr(c)) | P(equatype(b,a)). ** KEPT: 75 (41,11) Answer(Y) | P(equatype(b,a)) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 76 (41,9,35) Answer(Y) | P(equatype(b,a)) | P(atr(b)) | P(liar(a)). ** KEPT: 77 (41,8,20,1) Answer(Y) | P(equatype(b,a)) | P(equatype(a,c)) | P(liar(a)). ** KEPT: 78 (41,10,67) Answer(Y) | P(atr(c)) | P(liar(a)). 78 back subsumes: 45 (32,9,1) Answer(Y) | P(atr(c)) | P(atr(b)) | P(liar(a)). new given clause: 78 (41,10,67) Answer(Y) | P(atr(c)) | P(liar(a)). ** KEPT: 79 (78,11) Answer(Y) | P(liar(a)) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 80 (78,9,35) Answer(Y) | P(liar(a)) | P(atr(b)). ** KEPT: 81 (78,8,20,1) Answer(Y) | P(liar(a)) | P(equatype(a,c)). ** KEPT: 82 (78,12) Answer(Y) | P(atr(c)) | P(equatype(a,x)) | P(atr(x)). 80 back subsumes: 76 (41,9,35) Answer(Y) | P(equatype(b,a)) | P(atr(b)) | P(liar(a)). 80 back subsumes: 48 (32,9,35) P(equatype(a,b)) | Answer(Y) | P(atr(b)) | P(liar(a)). 81 back subsumes: 77 (41,8,20,1) Answer(Y) | P(equatype(b,a)) | P(equatype(a,c)) | P(liar(a)). 81 back subsumes: 49 (32,8,20,1) P(equatype(a,b)) | Answer(Y) | P(equatype(a,c)) | P(liar(a)). new given clause: 80 (78,9,35) Answer(Y) | P(liar(a)) | P(atr(b)). ** KEPT: 83 (80,12) Answer(Y) | P(atr(b)) | P(equatype(a,x)) | P(atr(x)). ** KEPT: 84 (80,11) Answer(Y) | P(liar(a)) | P(equatype(b,x)) | P(liar(x)). ** KEPT: 85 (80,8,19,1) Answer(Y) | P(liar(a)) | P(equatype(a,b)). new given clause: 56 (33,13) Answer(N) | P(liar(c)) | P(equatype(b,a)). ** KEPT: 86 (56,12) Answer(N) | P(equatype(b,a)) | P(equatype(c,x)) | P(atr(x)). ** KEPT: 87 (56,10,35) Answer(N) | P(equatype(b,a)) | P(liar(b)) | P(liar(a)). ** KEPT: 88 (56,7,20,35) Answer(N) | P(equatype(b,a)) | P(equatype(a,c)) | P(equatype(c,b)). ** KEPT: 89 (56,7,20,34) Answer(N) | P(equatype(b,a)) | P(equatype(a,c)) | P(equatype(b,c)). ** KEPT: 90 (56,7,20,1) Answer(N) | P(equatype(b,a)) | P(equatype(a,c)) | P(atr(a)). ** KEPT: 91 (56,7,18,1) Answer(N) | P(equatype(b,a)) | P(equatype(b,c)) | P(atr(b)). new given clause: 72 (67,8,18,1) P(liar(b)) | Answer(Y) | P(equatype(b,c)). ** KEPT: 92 (72,12) Answer(Y) | P(equatype(b,c)) | P(equatype(b,x)) | P(atr(x)). ** KEPT: 93 (72,7,19,35) Answer(Y) | P(equatype(b,c)) | P(equatype(a,b)) | P(equatype(c,b)). ** KEPT: 94 (72,7,19,34) Answer(Y) | P(equatype(b,c)) | P(equatype(a,b)). ** KEPT: 95 (72,5,1,22) P(liar(b)) | Answer(Y) | P(atr(a)). 94 back subsumes: 93 (72,7,19,35) Answer(Y) | P(equatype(b,c)) | P(equatype(a,b)) | P(equatype(c,b)). new given clause: 95 (72,5,1,22) P(liar(b)) | Answer(Y) | P(atr(a)). ** KEPT: 96 (95,12) Answer(Y) | P(atr(a)) | P(equatype(b,x)) | P(atr(x)). ** KEPT: 97 (95,7,19,35) Answer(Y) | P(atr(a)) | P(equatype(a,b)) | P(equatype(c,b)). ** KEPT: 98 (95,7,19,1) Answer(Y) | P(atr(a)) | P(equatype(a,b)). ** KEPT: 99 (95,11) P(liar(b)) | Answer(Y) | P(equatype(a,x)) | P(liar(x)). ** KEPT: 100 (95,8,20,67) P(liar(b)) | Answer(Y) | P(equatype(a,c)). 98 back subsumes: 97 (95,7,19,35) Answer(Y) | P(atr(a)) | P(equatype(a,b)) | P(equatype(c,b)). new given clause: 74 (67,7,21,1) P(atr(c)) | Answer(Y) | P(equatype(c,b)). ** KEPT: 101 (74,11) Answer(Y) | P(equatype(c,b)) | P(equatype(c,x)) | P(liar(x)). new given clause: 81 (78,8,20,1) Answer(Y) | P(liar(a)) | P(equatype(a,c)). ** KEPT: 102 (81,12) Answer(Y) | P(equatype(a,c)) | P(equatype(a,x)) | P(atr(x)). new given clause: 85 (80,8,19,1) Answer(Y) | P(liar(a)) | P(equatype(a,b)). ** KEPT: 103 (85,12) Answer(Y) | P(equatype(a,b)) | P(equatype(a,x)) | P(atr(x)). ** KEPT: 104 (85,14,23,78) Answer(Y) | P(liar(a)). 104 back subsumes: 85 (80,8,19,1) Answer(Y) | P(liar(a)) | P(equatype(a,b)). 104 back subsumes: 84 (80,11) Answer(Y) | P(liar(a)) | P(equatype(b,x)) | P(liar(x)). 104 back subsumes: 81 (78,8,20,1) Answer(Y) | P(liar(a)) | P(equatype(a,c)). 104 back subsumes: 80 (78,9,35) Answer(Y) | P(liar(a)) | P(atr(b)). 104 back subsumes: 79 (78,11) Answer(Y) | P(liar(a)) | P(equatype(c,x)) | P(liar(x)). 104 back subsumes: 78 (41,10,67) Answer(Y) | P(atr(c)) | P(liar(a)). new given clause: 104 (85,14,23,78) Answer(Y) | P(liar(a)). ** KEPT: 105 (104,12) Answer(Y) | P(equatype(a,x)) | P(atr(x)). ** KEPT: 106 (104,5,22,72) Answer(Y) | P(liar(b)). 105 back subsumes: 103 (85,12) Answer(Y) | P(equatype(a,b)) | P(equatype(a,x)) | P(atr(x)). 105 back subsumes: 102 (81,12) Answer(Y) | P(equatype(a,c)) | P(equatype(a,x)) | P(atr(x)). 105 back subsumes: 83 (80,12) Answer(Y) | P(atr(b)) | P(equatype(a,x)) | P(atr(x)). 105 back subsumes: 82 (78,12) Answer(Y) | P(atr(c)) | P(equatype(a,x)) | P(atr(x)). 106 back subsumes: 100 (95,8,20,67) P(liar(b)) | Answer(Y) | P(equatype(a,c)). 106 back subsumes: 99 (95,11) P(liar(b)) | Answer(Y) | P(equatype(a,x)) | P(liar(x)). 106 back subsumes: 95 (72,5,1,22) P(liar(b)) | Answer(Y) | P(atr(a)). 106 back subsumes: 72 (67,8,18,1) P(liar(b)) | Answer(Y) | P(equatype(b,c)). 106 back subsumes: 71 (67,11) P(liar(b)) | Answer(Y) | P(equatype(c,x)) | P(liar(x)). 106 back subsumes: 67 (37,10,32) P(atr(c)) | P(liar(b)) | Answer(Y). new given clause: 106 (104,5,22,72) Answer(Y) | P(liar(b)). ** KEPT: 107 (106,12) Answer(Y) | P(equatype(b,x)) | P(atr(x)). ** KEPT: 108 (106,7,19,104) Answer(Y) | P(equatype(a,b)). 107 back subsumes: 96 (95,12) Answer(Y) | P(atr(a)) | P(equatype(b,x)) | P(atr(x)). 107 back subsumes: 92 (72,12) Answer(Y) | P(equatype(b,c)) | P(equatype(b,x)) | P(atr(x)). 107 back subsumes: 73 (67,12) P(atr(c)) | Answer(Y) | P(equatype(b,x)) | P(atr(x)). 108 back subsumes: 98 (95,7,19,1) Answer(Y) | P(atr(a)) | P(equatype(a,b)). 108 back subsumes: 94 (72,7,19,34) Answer(Y) | P(equatype(b,c)) | P(equatype(a,b)). 108 back subsumes: 47 (32,11) P(equatype(a,b)) | Answer(Y) | P(equatype(c,x)) | P(liar(x)). 108 back subsumes: 32 (23,17,1) P(equatype(a,b)) | Answer(Y) | P(atr(c)). new given clause: 108 (106,7,19,104) Answer(Y) | P(equatype(a,b)). ** KEPT: 109 (108,14,23,74) Answer(Y) | P(equatype(c,b)). ** KEPT: 110 (108,14,23,41) Answer(Y) | P(equatype(b,a)). ** KEPT: 111 (108,14,23,1) Answer(Y) | P(liar(c)). 109 back subsumes: 101 (74,11) Answer(Y) | P(equatype(c,b)) | P(equatype(c,x)) | P(liar(x)). 109 back subsumes: 74 (67,7,21,1) P(atr(c)) | Answer(Y) | P(equatype(c,b)). 110 back subsumes: 75 (41,11) Answer(Y) | P(equatype(b,a)) | P(equatype(c,x)) | P(liar(x)). 110 back subsumes: 41 (32,13) Answer(Y) | P(atr(c)) | P(equatype(b,a)). new given clause: 111 (108,14,23,1) Answer(Y) | P(liar(c)). ** KEPT: 112 (111,12) Answer(Y) | P(equatype(c,x)) | P(atr(x)). ** KEPT: 113 (111,7,20,104) Answer(Y) | P(equatype(a,c)). ** KEPT: 114 (111,7,18,106) Answer(Y) | P(equatype(b,c)). new given clause: 109 (108,14,23,74) Answer(Y) | P(equatype(c,b)). new given clause: 110 (108,14,23,41) Answer(Y) | P(equatype(b,a)). new given clause: 113 (111,7,20,104) Answer(Y) | P(equatype(a,c)). ** KEPT: 115 (113,13) Answer(Y) | P(equatype(c,a)). new given clause: 114 (111,7,18,106) Answer(Y) | P(equatype(b,c)). ** KEPT: 116 (114,5,104,22) Answer(Y). 116 back subsumes: 115 (113,13) Answer(Y) | P(equatype(c,a)). 116 back subsumes: 114 (111,7,18,106) Answer(Y) | P(equatype(b,c)). 116 back subsumes: 113 (111,7,20,104) Answer(Y) | P(equatype(a,c)). 116 back subsumes: 112 (111,12) Answer(Y) | P(equatype(c,x)) | P(atr(x)). 116 back subsumes: 111 (108,14,23,1) Answer(Y) | P(liar(c)). 116 back subsumes: 110 (108,14,23,41) Answer(Y) | P(equatype(b,a)). 116 back subsumes: 109 (108,14,23,74) Answer(Y) | P(equatype(c,b)). 116 back subsumes: 108 (106,7,19,104) Answer(Y) | P(equatype(a,b)). 116 back subsumes: 107 (106,12) Answer(Y) | P(equatype(b,x)) | P(atr(x)). 116 back subsumes: 106 (104,5,22,72) Answer(Y) | P(liar(b)). 116 back subsumes: 105 (104,12) Answer(Y) | P(equatype(a,x)) | P(atr(x)). 116 back subsumes: 104 (85,14,23,78) Answer(Y) | P(liar(a)). 116 back subsumes: 55 (46,14,23,40) Answer(Y) | Answer(N). 116 back subsumes: 17 -Q(x,y) | -P(liar(x)) | P(y) | Answer(Y). 116 back subsumes: 14 -Q(x,y) | -P(atr(x)) | -P(y) | Answer(Y). new given clause: 116 (114,5,104,22) Answer(Y). new given clause: 24 (18,8,1,1) P(equatype(b,c)) | P(liar(b)) | P(liar(c)). ** KEPT: 117 (24,5,1,22) P(liar(b)) | P(liar(c)) | P(atr(a)). ** KEPT: 118 (24,12) P(equatype(b,c)) | P(liar(c)) | P(equatype(b,x)) | P(atr(x)). ** KEPT: 119 (24,7,19,35) P(equatype(b,c)) | P(liar(c)) | P(equatype(a,b)) | P(equatype(c,b)). ** KEPT: 120 (24,7,19,34) P(equatype(b,c)) | P(liar(c)) | P(equatype(a,b)). ** KEPT: 121 (24,12) P(equatype(b,c)) | P(liar(b)) | P(equatype(c,x)) | P(atr(x)). ** KEPT: 122 (24,7,20,35) P(equatype(b,c)) | P(liar(b)) | P(equatype(a,c)) | P(equatype(c,b)). ** KEPT: 123 (24,7,20,34) P(equatype(b,c)) | P(liar(b)) | P(equatype(a,c)). 117 back subsumes: 57 (33,10,1) Answer(N) | P(liar(c)) | P(liar(b)) | P(atr(a)). 120 back subsumes: 119 (24,7,19,35) P(equatype(b,c)) | P(liar(c)) | P(equatype(a,b)) | P(equatype(c,b)). 123 back subsumes: 122 (24,7,20,35) P(equatype(b,c)) | P(liar(b)) | P(equatype(a,c)) | P(equatype(c,b)). new given clause: 117 (24,5,1,22) P(liar(b)) | P(liar(c)) | P(atr(a)). ** KEPT: 124 (117,12) P(liar(c)) | P(atr(a)) | P(equatype(b,x)) | P(atr(x)). ** KEPT: 125 (117,7,19,35) P(liar(c)) | P(atr(a)) | P(equatype(a,b)) | P(equatype(c,b)). ** KEPT: 126 (117,7,19,1) P(liar(c)) | P(atr(a)) | P(equatype(a,b)). ** KEPT: 127 (117,12) P(liar(b)) | P(atr(a)) | P(equatype(c,x)) | P(atr(x)). ** KEPT: 128 (117,7,20,35) P(liar(b)) | P(atr(a)) | P(equatype(a,c)) | P(equatype(c,b)). ** KEPT: 129 (117,7,20,1) P(liar(b)) | P(atr(a)) | P(equatype(a,c)). ** KEPT: 130 (117,11) P(liar(b)) | P(liar(c)) | P(equatype(a,x)) | P(liar(x)). 126 back subsumes: 125 (117,7,19,35) P(liar(c)) | P(atr(a)) | P(equatype(a,b)) | P(equatype(c,b)). 129 back subsumes: 128 (117,7,20,35) P(liar(b)) | P(atr(a)) | P(equatype(a,c)) | P(equatype(c,b)). new given clause: 25 (18,7,1,1) P(equatype(b,c)) | P(atr(b)) | P(atr(c)). ** KEPT: 131 (25,5,1,22) P(atr(b)) | P(atr(c)) | P(atr(a)). ** KEPT: 132 (25,11) P(equatype(b,c)) | P(atr(c)) | P(equatype(b,x)) | P(liar(x)). ** KEPT: 133 (25,11) P(equatype(b,c)) | P(atr(b)) | P(equatype(c,x)) | P(liar(x)). new given clause: 131 (25,5,1,22) P(atr(b)) | P(atr(c)) | P(atr(a)). ** KEPT: 134 (131,11) P(atr(c)) | P(atr(a)) | P(equatype(b,x)) | P(liar(x)). ** KEPT: 135 (131,11) P(atr(b)) | P(atr(a)) | P(equatype(c,x)) | P(liar(x)). ** KEPT: 136 (131,2,56) P(atr(b)) | P(atr(a)) | Answer(N) | P(equatype(b,a)). ** KEPT: 137 (131,11) P(atr(b)) | P(atr(c)) | P(equatype(a,x)) | P(liar(x)). new given clause: 26 (19,8,1,1) P(equatype(a,b)) | P(liar(a)) | P(liar(b)). ** KEPT: 138 (26,13) P(liar(a)) | P(liar(b)) | P(equatype(b,a)). ** KEPT: 139 (26,12) P(equatype(a,b)) | P(liar(b)) | P(equatype(a,x)) | P(atr(x)). ** KEPT: 140 (26,7,20,56) P(equatype(a,b)) | P(liar(b)) | P(equatype(a,c)) | Answer(N) | P(equatype(b,a)). ** KEPT: 141 (26,7,20,33) P(equatype(a,b)) | P(liar(b)) | P(equatype(a,c)) | Answer(N). ** KEPT: 142 (26,12) P(equatype(a,b)) | P(liar(a)) | P(equatype(b,x)) | P(atr(x)). 138 back subsumes: 87 (56,10,35) Answer(N) | P(equatype(b,a)) | P(liar(b)) | P(liar(a)). 141 back subsumes: 140 (26,7,20,56) P(equatype(a,b)) | P(liar(b)) | P(equatype(a,c)) | Answer(N) | P(equatype(b,a)). new given clause: 27 (19,7,1,1) P(equatype(a,b)) | P(atr(a)) | P(atr(b)). ** KEPT: 143 (27,13) P(atr(a)) | P(atr(b)) | P(equatype(b,a)). ** KEPT: 144 (27,11) P(equatype(a,b)) | P(atr(b)) | P(equatype(a,x)) | P(liar(x)). ** KEPT: 145 (27,11) P(equatype(a,b)) | P(atr(a)) | P(equatype(b,x)) | P(liar(x)). 143 back subsumes: 136 (131,2,56) P(atr(b)) | P(atr(a)) | Answer(N) | P(equatype(b,a)). ------------ END OF SEARCH ------------ search stopped by max_given option. --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 40). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 23 clauses given 40 clauses generated 900 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 778 (clauses subsumed by sos) 324 unit deletions 0 clauses kept 122 empty clauses 0 factors generated 0 clauses back subsumed 67 clauses not processed 0 ----------- times (seconds) ----------- run time 12.80 input time 0.30 binary_res time 0.00 hyper_res time 2.93 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 8.02 demod time 0.00 weigh time 0.05 for_sub time 6.21 unit_del time 0.00 post_process time 1.14 back_sub time 0.67 conflict time 0.01 factor time 0.00 FPA build time 0.26 IS build time 0.10 print_cl time 0.84 cl integrate time 0.12 window time 0.00 SHAR_EOF if test -f 'tandl39.desc' then echo shar: over-writing existing file "'tandl39.desc'" fi cat << \SHAR_EOF > 'tandl39.desc' problem-set/puzzles/truth_lies/tandl39.desc created : 09/03/86 revised : 07/18/88 Natural Language Description: Truthteller and Liars Puzzle #39 There is an island with exactly three types of people -- truthtellers who always tell the truth, and liars who always lie, and normals who sometimes tell the truth and sometimes lie. We are given three people, A, B, C, one of whom is a truthteller, one a liar, and one a normal (but not necc on that order ). They make the following statements. A: I am normal; B: That is true. C: I am not normal . What are A,B, and C ? Versions: tandl39.ver1 : Declarative representation, using hyper-resolution. answer: A is a liar, B is a normal, and C is a truthteller. created by : Swaminathan verified for ITP : 09/03/86 translated for OTTER by : K.R. verified for OTTER : 07/18/88 SHAR_EOF if test -f 'tandl39.ver1.clauses' then echo shar: over-writing existing file "'tandl39.ver1.clauses'" fi cat << \SHAR_EOF > 'tandl39.ver1.clauses' % problem-set/puzzles/truth_lies/tandl39.ver1.clauses % created : 07/14/88 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #39" using hyper- % resolution. % % Truthteller and Liars Puzzle #39 % % There is an island with exactly three types of people -- % truthtellers who always tell the truth, and liars who always % lie, and normals who sometimes tell the truth and sometimes lie. % We are given three people, A, B, C, one of whom is a % truthteller, one a liar, and one a normal (but not necc on that % order ). They make the following statements. % A: I am normal; B: That is true. C: I am not normal . % What are A,B, and C? % representation: % % declare_predicate(3,P). % declare_predicate(1,TRUE). % declare_functions(1,[atr,liar,norm,nnorm]). % declare_function(2,fsaid). % declare_variables([x,y,z]). % declare_constants([a,b,c]). % % TRUE(x) means "x is true" % P(x,y,z) means x,y, and z are persons under consideration % asaid(x,y) means "x made the statement y " % atr(x) means "x is a truthteller" % liar(x) means "x is a liar" % norm(x) means "x is a normal" % A person is exclusively a truthteller or liar or a normal TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(liar(x)) | -TRUE(norm(x)). % A truthteller always says the truth and a liar lies % Since a normal is allowed to do both, no clause exists -TRUE(atr(x)) | -TRUE(fsaid(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(fsaid(x,y)) | -TRUE(y) . % if a statement is true then it has to be made by a % truthteller or a normal. -TRUE(x) | -TRUE(fsaid(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). TRUE(x) | -TRUE(fsaid(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). % Definition of "not normal" (nnorm) -TRUE(nnorm(x)) | -TRUE(norm(x)). TRUE(nnorm(x)) | TRUE(norm(x)). % Only one of A, B, and C is a truthteller, one a liar % and one a normal -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(y)). -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(z)). -P(x,y,z) | -TRUE(liar(x)) | -TRUE(liar(y)). -P(x,y,z) | -TRUE(liar(x)) | -TRUE(liar(z)). -P(x,y,z) | -TRUE(norm(x)) | -TRUE(norm(y)). -P(x,y,z) | -TRUE(norm(x)) | -TRUE(norm(z)). % P stands for persons in the puzzle P(a,b,c). P(b,c,a). P(c,b,a). % statements made by A, B and C TRUE(fsaid(a,norm(a))). TRUE(fsaid(b,norm(a))). TRUE(fsaid(c,nnorm(c))). SHAR_EOF if test -f 'tandl39.ver1.in' then echo shar: over-writing existing file "'tandl39.ver1.in'" fi cat << \SHAR_EOF > 'tandl39.ver1.in' % problem-set/puzzles/truth_lies/tandl39.ver1.in % created : 09/03/86 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #39" using hyper- % resolution. % % Truthteller and Liars Puzzle #39 % % There is an island with exactly three types of people -- % truthtellers who always tell the truth, and liars who always % lie, and normals who sometimes tell the truth and sometimes lie. % We are given three people, A, B, C, one of whom is a % truthteller, one a liar, and one a normal (but not necc on that % order ). They make the following statements. % A: I am normal; B: That is true. C: I am not normal . % What are A,B, and C? % representation: % % declare_predicate(3,P). % declare_predicate(1,TRUE). % declare_functions(1,[atr,liar,norm,nnorm]). % declare_function(2,fsaid). % declare_variables([x,y,z]). % declare_constants([a,b,c]). % % TRUE(x) means "x is true" % P(x,y,z) means x,y, and z are persons under consideration % asaid(x,y) means "x made the statement y " % atr(x) means "x is a truthteller" % liar(x) means "x is a liar" % norm(x) means "x is a normal" set(hyper_res). list(axioms). % A person is exclusively a truthteller or liar or a normal TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(liar(x)) | -TRUE(norm(x)). % A truthteller always says the truth and a liar lies % Since a normal is allowed to do both, no clause exists -TRUE(atr(x)) | -TRUE(fsaid(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(fsaid(x,y)) | -TRUE(y) . % if a statement is true then it has to be made by a % truthteller or a normal. -TRUE(x) | -TRUE(fsaid(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). TRUE(x) | -TRUE(fsaid(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). % Definition of "not normal" (nnorm) -TRUE(nnorm(x)) | -TRUE(norm(x)). TRUE(nnorm(x)) | TRUE(norm(x)). % Only one of A, B, and C is a truthteller, one a liar % and one a normal -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(y)). -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(z)). -P(x,y,z) | -TRUE(liar(x)) | -TRUE(liar(y)). -P(x,y,z) | -TRUE(liar(x)) | -TRUE(liar(z)). -P(x,y,z) | -TRUE(norm(x)) | -TRUE(norm(y)). -P(x,y,z) | -TRUE(norm(x)) | -TRUE(norm(z)). end_of_list. list(sos). % P stands for persons in the puzzle P(a,b,c). P(b,c,a). P(c,b,a). % statements made by A, B and C TRUE(fsaid(a,norm(a))). TRUE(fsaid(b,norm(a))). TRUE(fsaid(c,nnorm(c))). end_of_list. SHAR_EOF if test -f 'tandl39.ver1.out' then echo shar: over-writing existing file "'tandl39.ver1.out'" fi cat << \SHAR_EOF > 'tandl39.ver1.out' problem-set/puzzles/truth_lies/tandl39.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). 2 -TRUE(atr(x)) | -TRUE(norm(x)). 3 -TRUE(atr(x)) | -TRUE(liar(x)). 4 -TRUE(liar(x)) | -TRUE(norm(x)). 5 -TRUE(atr(x)) | -TRUE(fsaid(x,y)) | TRUE(y). 6 -TRUE(liar(x)) | -TRUE(fsaid(x,y)) | -TRUE(y). 7 -TRUE(x) | -TRUE(fsaid(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). 8 TRUE(x) | -TRUE(fsaid(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). 9 -TRUE(nnorm(x)) | -TRUE(norm(x)). 10 TRUE(nnorm(x)) | TRUE(norm(x)). 11 -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(y)). 12 -P(x,y,z) | -TRUE(atr(x)) | -TRUE(atr(z)). 13 -P(x,y,z) | -TRUE(liar(x)) | -TRUE(liar(y)). 14 -P(x,y,z) | -TRUE(liar(x)) | -TRUE(liar(z)). 15 -P(x,y,z) | -TRUE(norm(x)) | -TRUE(norm(y)). 16 -P(x,y,z) | -TRUE(norm(x)) | -TRUE(norm(z)). end_of_list. list(sos). 17 P(a,b,c). 18 P(b,c,a). 19 P(c,b,a). 20 TRUE(fsaid(a,norm(a))). 21 TRUE(fsaid(b,norm(a))). 22 TRUE(fsaid(c,nnorm(c))). end_of_list. new given clause: 17 P(a,b,c). ** KEPT: 23 (17,16,10,10) TRUE(nnorm(a)) | TRUE(nnorm(c)). ** KEPT: 24 (17,16,10,1) TRUE(nnorm(a)) | TRUE(atr(c)) | TRUE(liar(c)). ** KEPT: 25 (17,16,1,10) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(nnorm(c)). ** KEPT: 26 (17,16,1,1) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(atr(c)) | TRUE(liar(c)). ** KEPT: 27 (17,15,10,10) TRUE(nnorm(a)) | TRUE(nnorm(b)). ** KEPT: 28 (17,15,10,1) TRUE(nnorm(a)) | TRUE(atr(b)) | TRUE(liar(b)). ** KEPT: 29 (17,15,1,10) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(nnorm(b)). ** KEPT: 30 (17,15,1,1) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(atr(b)) | TRUE(liar(b)). ** KEPT: 31 (17,14,1,1) TRUE(atr(a)) | TRUE(norm(a)) | TRUE(atr(c)) | TRUE(norm(c)). ** KEPT: 32 (17,13,1,1) TRUE(atr(a)) | TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). ** KEPT: 33 (17,12,1,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(liar(c)) | TRUE(norm(c)). ** KEPT: 34 (17,11,1,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(liar(b)) | TRUE(norm(b)). new given clause: 18 P(b,c,a). ** KEPT: 35 (18,15,10,10) TRUE(nnorm(b)) | TRUE(nnorm(c)). ** KEPT: 36 (18,15,10,1) TRUE(nnorm(b)) | TRUE(atr(c)) | TRUE(liar(c)). ** KEPT: 37 (18,15,1,10) TRUE(atr(b)) | TRUE(liar(b)) | TRUE(nnorm(c)). ** KEPT: 38 (18,15,1,1) TRUE(atr(b)) | TRUE(liar(b)) | TRUE(atr(c)) | TRUE(liar(c)). ** KEPT: 39 (18,13,1,1) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(atr(c)) | TRUE(norm(c)). ** KEPT: 40 (18,11,1,1) TRUE(liar(b)) | TRUE(norm(b)) | TRUE(liar(c)) | TRUE(norm(c)). new given clause: 19 P(c,b,a). new given clause: 20 TRUE(fsaid(a,norm(a))). ** KEPT: 41 (20,8) TRUE(norm(a)) | TRUE(liar(a)). 41 back subsumes: 34 (17,11,1,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(liar(b)) | TRUE(norm(b)). 41 back subsumes: 33 (17,12,1,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(liar(c)) | TRUE(norm(c)). new given clause: 21 TRUE(fsaid(b,norm(a))). ** KEPT: 42 (21,8) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(norm(b)). ** KEPT: 43 (21,7,10) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(nnorm(a)). ** KEPT: 44 (21,7,1) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(atr(a)) | TRUE(liar(a)). new given clause: 22 TRUE(fsaid(c,nnorm(c))). ** KEPT: 45 (22,7,10) TRUE(atr(c)) | TRUE(norm(c)). 45 back subsumes: 39 (18,13,1,1) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(atr(c)) | TRUE(norm(c)). 45 back subsumes: 31 (17,14,1,1) TRUE(atr(a)) | TRUE(norm(a)) | TRUE(atr(c)) | TRUE(norm(c)). new given clause: 23 (17,16,10,10) TRUE(nnorm(a)) | TRUE(nnorm(c)). new given clause: 27 (17,15,10,10) TRUE(nnorm(a)) | TRUE(nnorm(b)). new given clause: 35 (18,15,10,10) TRUE(nnorm(b)) | TRUE(nnorm(c)). new given clause: 41 (20,8) TRUE(norm(a)) | TRUE(liar(a)). ** KEPT: 46 (41,16,19,10) TRUE(liar(a)) | TRUE(nnorm(c)). ** KEPT: 47 (41,16,19,1) TRUE(liar(a)) | TRUE(atr(c)) | TRUE(liar(c)). ** KEPT: 48 (41,16,18,10) TRUE(liar(a)) | TRUE(nnorm(b)). ** KEPT: 49 (41,16,18,1) TRUE(liar(a)) | TRUE(atr(b)) | TRUE(liar(b)). ** KEPT: 50 (41,7,21) TRUE(liar(a)) | TRUE(atr(b)) | TRUE(norm(b)). ** KEPT: 51 (41,14,18,1) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). 46 back subsumes: 25 (17,16,1,10) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(nnorm(c)). 47 back subsumes: 26 (17,16,1,1) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(atr(c)) | TRUE(liar(c)). 48 back subsumes: 29 (17,15,1,10) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(nnorm(b)). 49 back subsumes: 30 (17,15,1,1) TRUE(atr(a)) | TRUE(liar(a)) | TRUE(atr(b)) | TRUE(liar(b)). 50 back subsumes: 44 (21,7,1) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(atr(a)) | TRUE(liar(a)). 51 back subsumes: 32 (17,13,1,1) TRUE(atr(a)) | TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). new given clause: 45 (22,7,10) TRUE(atr(c)) | TRUE(norm(c)). ** KEPT: 52 (45,11,18,1) TRUE(norm(c)) | TRUE(liar(b)) | TRUE(norm(b)). ** KEPT: 53 (45,16,17,41) TRUE(atr(c)) | TRUE(liar(a)). ** KEPT: 54 (45,16,17,10) TRUE(atr(c)) | TRUE(nnorm(a)). ** KEPT: 55 (45,15,18,10) TRUE(atr(c)) | TRUE(nnorm(b)). ** KEPT: 56 (45,15,18,1) TRUE(atr(c)) | TRUE(atr(b)) | TRUE(liar(b)). 52 back subsumes: 40 (18,11,1,1) TRUE(liar(b)) | TRUE(norm(b)) | TRUE(liar(c)) | TRUE(norm(c)). 53 back subsumes: 47 (41,16,19,1) TRUE(liar(a)) | TRUE(atr(c)) | TRUE(liar(c)). 54 back subsumes: 24 (17,16,10,1) TRUE(nnorm(a)) | TRUE(atr(c)) | TRUE(liar(c)). 55 back subsumes: 36 (18,15,10,1) TRUE(nnorm(b)) | TRUE(atr(c)) | TRUE(liar(c)). 56 back subsumes: 38 (18,15,1,1) TRUE(atr(b)) | TRUE(liar(b)) | TRUE(atr(c)) | TRUE(liar(c)). new given clause: 46 (41,16,19,10) TRUE(liar(a)) | TRUE(nnorm(c)). ** KEPT: 57 (46,14,18,1) TRUE(nnorm(c)) | TRUE(atr(b)) | TRUE(norm(b)). new given clause: 48 (41,16,18,10) TRUE(liar(a)) | TRUE(nnorm(b)). new given clause: 53 (45,16,17,41) TRUE(atr(c)) | TRUE(liar(a)). ** KEPT: 58 (53,11,18,1) TRUE(liar(a)) | TRUE(liar(b)) | TRUE(norm(b)). ** KEPT: 59 (53,14,18,1) TRUE(atr(c)) | TRUE(atr(b)) | TRUE(norm(b)). new given clause: 54 (45,16,17,10) TRUE(atr(c)) | TRUE(nnorm(a)). ** KEPT: 60 (54,11,18,1) TRUE(nnorm(a)) | TRUE(liar(b)) | TRUE(norm(b)). new given clause: 55 (45,15,18,10) TRUE(atr(c)) | TRUE(nnorm(b)). new given clause: 28 (17,15,10,1) TRUE(nnorm(a)) | TRUE(atr(b)) | TRUE(liar(b)). ** KEPT: 61 (28,11,19,54) TRUE(nnorm(a)) | TRUE(liar(b)). ** KEPT: 62 (28,6,21,41) TRUE(nnorm(a)) | TRUE(atr(b)) | TRUE(liar(a)). ** KEPT: 63 (28,6,21,10) TRUE(nnorm(a)) | TRUE(atr(b)). 61 back subsumes: 60 (54,11,18,1) TRUE(nnorm(a)) | TRUE(liar(b)) | TRUE(norm(b)). 61 back subsumes: 28 (17,15,10,1) TRUE(nnorm(a)) | TRUE(atr(b)) | TRUE(liar(b)). 63 back subsumes: 62 (28,6,21,41) TRUE(nnorm(a)) | TRUE(atr(b)) | TRUE(liar(a)). 63 back subsumes: 43 (21,7,10) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(nnorm(a)). new given clause: 61 (28,11,19,54) TRUE(nnorm(a)) | TRUE(liar(b)). ** KEPT: 64 (61,9,41) TRUE(liar(b)) | TRUE(liar(a)). ** KEPT: 65 (61,6,21,41) TRUE(nnorm(a)) | TRUE(liar(a)). ** KEPT: 66 (61,6,21,10) TRUE(nnorm(a)). 64 back subsumes: 58 (53,11,18,1) TRUE(liar(a)) | TRUE(liar(b)) | TRUE(norm(b)). 64 back subsumes: 49 (41,16,18,1) TRUE(liar(a)) | TRUE(atr(b)) | TRUE(liar(b)). 66 back subsumes: 65 (61,6,21,41) TRUE(nnorm(a)) | TRUE(liar(a)). 66 back subsumes: 63 (28,6,21,10) TRUE(nnorm(a)) | TRUE(atr(b)). 66 back subsumes: 61 (28,11,19,54) TRUE(nnorm(a)) | TRUE(liar(b)). 66 back subsumes: 54 (45,16,17,10) TRUE(atr(c)) | TRUE(nnorm(a)). 66 back subsumes: 27 (17,15,10,10) TRUE(nnorm(a)) | TRUE(nnorm(b)). 66 back subsumes: 23 (17,16,10,10) TRUE(nnorm(a)) | TRUE(nnorm(c)). new given clause: 66 (61,6,21,10) TRUE(nnorm(a)). ** KEPT: 67 (66,9,41) TRUE(liar(a)). 67 back subsumes: 64 (61,9,41) TRUE(liar(b)) | TRUE(liar(a)). 67 back subsumes: 53 (45,16,17,41) TRUE(atr(c)) | TRUE(liar(a)). 67 back subsumes: 50 (41,7,21) TRUE(liar(a)) | TRUE(atr(b)) | TRUE(norm(b)). 67 back subsumes: 48 (41,16,18,10) TRUE(liar(a)) | TRUE(nnorm(b)). 67 back subsumes: 46 (41,16,19,10) TRUE(liar(a)) | TRUE(nnorm(c)). 67 back subsumes: 41 (20,8) TRUE(norm(a)) | TRUE(liar(a)). new given clause: 67 (66,9,41) TRUE(liar(a)). ** KEPT: 68 (67,14,18,1) TRUE(atr(b)) | TRUE(norm(b)). 68 back subsumes: 59 (53,14,18,1) TRUE(atr(c)) | TRUE(atr(b)) | TRUE(norm(b)). 68 back subsumes: 57 (46,14,18,1) TRUE(nnorm(c)) | TRUE(atr(b)) | TRUE(norm(b)). 68 back subsumes: 51 (41,14,18,1) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). new given clause: 68 (67,14,18,1) TRUE(atr(b)) | TRUE(norm(b)). ** KEPT: 69 (68,11,19,45) TRUE(norm(b)) | TRUE(norm(c)). ** KEPT: 70 (68,5,21) TRUE(norm(b)) | TRUE(norm(a)). ** KEPT: 71 (68,15,19,45) TRUE(atr(b)) | TRUE(atr(c)). ** KEPT: 72 (68,15,19,10) TRUE(atr(b)) | TRUE(nnorm(c)). 69 back subsumes: 52 (45,11,18,1) TRUE(norm(c)) | TRUE(liar(b)) | TRUE(norm(b)). 70 back subsumes: 42 (21,8) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(norm(b)). 71 back subsumes: 56 (45,15,18,1) TRUE(atr(c)) | TRUE(atr(b)) | TRUE(liar(b)). 72 back subsumes: 37 (18,15,1,10) TRUE(atr(b)) | TRUE(liar(b)) | TRUE(nnorm(c)). new given clause: 69 (68,11,19,45) TRUE(norm(b)) | TRUE(norm(c)). new given clause: 70 (68,5,21) TRUE(norm(b)) | TRUE(norm(a)). ** KEPT: 73 (70,15,19,45) TRUE(norm(a)) | TRUE(atr(c)). ** KEPT: 74 (70,15,19,10) TRUE(norm(a)) | TRUE(nnorm(c)). ** KEPT: 75 (70,16,19,69) TRUE(norm(b)). 75 back subsumes: 70 (68,5,21) TRUE(norm(b)) | TRUE(norm(a)). 75 back subsumes: 69 (68,11,19,45) TRUE(norm(b)) | TRUE(norm(c)). 75 back subsumes: 68 (67,14,18,1) TRUE(atr(b)) | TRUE(norm(b)). new given clause: 75 (70,16,19,69) TRUE(norm(b)). ** KEPT: 76 (75,15,19,45) TRUE(atr(c)). ** KEPT: 77 (75,15,19,10) TRUE(nnorm(c)). 76 back subsumes: 73 (70,15,19,45) TRUE(norm(a)) | TRUE(atr(c)). 76 back subsumes: 71 (68,15,19,45) TRUE(atr(b)) | TRUE(atr(c)). 76 back subsumes: 55 (45,15,18,10) TRUE(atr(c)) | TRUE(nnorm(b)). 76 back subsumes: 45 (22,7,10) TRUE(atr(c)) | TRUE(norm(c)). 77 back subsumes: 74 (70,15,19,10) TRUE(norm(a)) | TRUE(nnorm(c)). 77 back subsumes: 72 (68,15,19,10) TRUE(atr(b)) | TRUE(nnorm(c)). 77 back subsumes: 35 (18,15,10,10) TRUE(nnorm(b)) | TRUE(nnorm(c)). new given clause: 76 (75,15,19,45) TRUE(atr(c)). new given clause: 77 (75,15,19,10) TRUE(nnorm(c)). ------------ END OF SEARCH ------------ sos empty. --------------- 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 22 clauses given 26 clauses generated 407 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 352 (clauses subsumed by sos) 138 unit deletions 0 clauses kept 55 empty clauses 0 factors generated 0 clauses back subsumed 50 clauses not processed 0 ----------- times (seconds) ----------- run time 2.92 input time 0.16 binary_res time 0.00 hyper_res time 1.16 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 1.12 demod time 0.00 weigh time 0.00 for_sub time 0.70 unit_del time 0.00 post_process time 0.36 back_sub time 0.20 conflict time 0.02 factor time 0.00 FPA build time 0.22 IS build time 0.04 print_cl time 0.18 cl integrate time 0.02 window time 0.00 SHAR_EOF if test -f 'tandl42.desc' then echo shar: over-writing existing file "'tandl42.desc'" fi cat << \SHAR_EOF > 'tandl42.desc' problem-set/puzzles/truth_lies/tandl42.desc created : 09/03/86 revised : 07/18/88 Natural Language Description: Truthtellers and Liars Puzzle #42 There is an island with exactly three types of people--truthtellers who always tell the truth, and liars who always lie, and normals who sometimes tell the truth and sometimes lie. Liars are said to be of the lowest rank , normals are middle rank, and truthtellers of the highest rank. Two people A and B on the island make the following statements. A: I am of lower rank than B B: That's not true! What are the ranks of A and B, and which of the two statements are true? Versions: tandl42.ver1 : Declarative representation, using hyper-resolution. answer: A is a normal and B is a normal. created by : Pillai verified for ITP : 09/03/86 translated for OTTER by : K.R. verified for OTTER : 07/18/88 SHAR_EOF if test -f 'tandl42.ver1.clauses' then echo shar: over-writing existing file "'tandl42.ver1.clauses'" fi cat << \SHAR_EOF > 'tandl42.ver1.clauses' % problem-set/puzzles/truth_lies/tandl42.ver1.clauses % created : 07/14/88 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #42" using hyper- % resolution. % % Truthtellers and Liars Puzzle #42 % % There is an island with exactly three types of people-- % truthtellers who always tell the truth, and liars who always % lie, and normals who sometimes tell the truth and sometimes % lie. Liars are said to be of the lowest rank , % normals are middle rank, and truthtellers of the highest rank % of the highest rank. Two people A and B on the island make the % following statements. % A: I am of lower rank than B % B: Thats not true! % What are the ranks of A and B, and which of the two statements % are true? % representation: % % declare_predicate(3,P). % declare_predicate(1,TRUE). % declare_functions(1,[atr,liar,norm,nnorm]). % declare_functions(2,[Said,lower,nlower]). % declare_variables([x,y,z]). % declare_constants([a,b,c]). % A person can be one of : truthteller, liar and normal TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(liar(x)) | -TRUE(norm(x)). % A truthteller always tells the truth and a liar always lies -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y) . -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). % Definition of "lower than" and "not lower than" TRUE(nlower(x,x)). -TRUE(nlower(x,y)) | -TRUE(lower(x,y)). TRUE(nlower(x,y)) | TRUE(lower(x,y)). -TRUE(lower(x,y)) | -TRUE(liar(x)) | TRUE(norm(y)) | TRUE(atr(y)). -TRUE(lower(x,y)) | -TRUE(norm(x)) | TRUE(atr(y)). -TRUE(lower(x,y)) | -TRUE(atr(x)). -TRUE(lower(x,y)) | -TRUE(atr(y)) | TRUE(norm(x)) | TRUE(liar(x)). -TRUE(lower(x,y)) | -TRUE(norm(y)) | TRUE(liar(x)). -TRUE(lower(x,y)) | -TRUE(liar(y)). -TRUE(nlower(x,y)) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(lower(y,x)). -TRUE(nlower(x,y)) | -TRUE(liar(x)) | TRUE(liar(y)) | TRUE(lower(y,x)). -TRUE(nlower(x,y)) | -TRUE(norm(x)) | TRUE(norm(y)) | TRUE(lower(y,x)). % Statements made by A and B TRUE(Said(a,lower(a,b))). TRUE(Said(b,nlower(a,b))). SHAR_EOF if test -f 'tandl42.ver1.in' then echo shar: over-writing existing file "'tandl42.ver1.in'" fi cat << \SHAR_EOF > 'tandl42.ver1.in' % problem-set/puzzles/truth_lies/tandl42.ver1.in % created : 09/03/86 % revised : 07/14/88 % description: % % This run solves "Truthtellers and Liars Puzzle #42" using hyper- % resolution. % % Truthtellers and Liars Puzzle #42 % % There is an island with exactly three types of people-- % truthtellers who always tell the truth, and liars who always % lie, and normals who sometimes tell the truth and sometimes % lie. Liars are said to be of the lowest rank , % normals are middle rank, and truthtellers of the highest rank % of the highest rank. Two people A and B on the island make the % following statements. % A: I am of lower rank than B % B: Thats not true! % What are the ranks of A and B, and which of the two statements % are true? % representation: % % declare_predicate(3,P). % declare_predicate(1,TRUE). % declare_functions(1,[atr,liar,norm,nnorm]). % declare_functions(2,[Said,lower,nlower]). % declare_variables([x,y,z]). % declare_constants([a,b,c]). set(hyper_res). assign(max_given,20). list(axioms). % A person can be one of : truthteller, liar and normal TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(norm(x)). -TRUE(atr(x)) | -TRUE(liar(x)). -TRUE(liar(x)) | -TRUE(norm(x)). % A truthteller always tells the truth and a liar always lies -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y) . -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y) . -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). % Definition of "lower than" and "not lower than" TRUE(nlower(x,x)). -TRUE(nlower(x,y)) | -TRUE(lower(x,y)). TRUE(nlower(x,y)) | TRUE(lower(x,y)). -TRUE(lower(x,y)) | -TRUE(liar(x)) | TRUE(norm(y)) | TRUE(atr(y)). -TRUE(lower(x,y)) | -TRUE(norm(x)) | TRUE(atr(y)). -TRUE(lower(x,y)) | -TRUE(atr(x)). -TRUE(lower(x,y)) | -TRUE(atr(y)) | TRUE(norm(x)) | TRUE(liar(x)). -TRUE(lower(x,y)) | -TRUE(norm(y)) | TRUE(liar(x)). -TRUE(lower(x,y)) | -TRUE(liar(y)). -TRUE(nlower(x,y)) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(lower(y,x)). -TRUE(nlower(x,y)) | -TRUE(liar(x)) | TRUE(liar(y)) | TRUE(lower(y,x)). -TRUE(nlower(x,y)) | -TRUE(norm(x)) | TRUE(norm(y)) | TRUE(lower(y,x)). end_of_list. list(sos). % Statements made by A and B TRUE(Said(a,lower(a,b))). TRUE(Said(b,nlower(a,b))). end_of_list. SHAR_EOF if test -f 'tandl42.ver1.out' then echo shar: over-writing existing file "'tandl42.ver1.out'" fi cat << \SHAR_EOF > 'tandl42.ver1.out' problem-set/puzzles/truth_lies/tandl42.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.9, 19 May 1988. set(hyper_res). assign(max_given,20). list(axioms). 1 TRUE(atr(x)) | TRUE(liar(x)) | TRUE(norm(x)). 2 -TRUE(atr(x)) | -TRUE(norm(x)). 3 -TRUE(atr(x)) | -TRUE(liar(x)). 4 -TRUE(liar(x)) | -TRUE(norm(x)). 5 -TRUE(atr(x)) | -TRUE(Said(x,y)) | TRUE(y). 6 -TRUE(liar(x)) | -TRUE(Said(x,y)) | -TRUE(y). 7 -TRUE(x) | -TRUE(Said(y,x)) | TRUE(atr(y)) | TRUE(norm(y)). 8 TRUE(x) | -TRUE(Said(y,x)) | TRUE(liar(y)) | TRUE(norm(y)). 9 TRUE(nlower(x,x)). 10 -TRUE(nlower(x,y)) | -TRUE(lower(x,y)). 11 TRUE(nlower(x,y)) | TRUE(lower(x,y)). 12 -TRUE(lower(x,y)) | -TRUE(liar(x)) | TRUE(norm(y)) | TRUE(atr(y)). 13 -TRUE(lower(x,y)) | -TRUE(norm(x)) | TRUE(atr(y)). 14 -TRUE(lower(x,y)) | -TRUE(atr(x)). 15 -TRUE(lower(x,y)) | -TRUE(atr(y)) | TRUE(norm(x)) | TRUE(liar(x)). 16 -TRUE(lower(x,y)) | -TRUE(norm(y)) | TRUE(liar(x)). 17 -TRUE(lower(x,y)) | -TRUE(liar(y)). 18 -TRUE(nlower(x,y)) | -TRUE(atr(x)) | TRUE(atr(y)) | TRUE(lower(y,x)). 19 -TRUE(nlower(x,y)) | -TRUE(liar(x)) | TRUE(liar(y)) | TRUE(lower(y,x)). 20 -TRUE(nlower(x,y)) | -TRUE(norm(x)) | TRUE(norm(y)) | TRUE(lower(y,x)). end_of_list. list(sos). 21 TRUE(Said(a,lower(a,b))). 22 TRUE(Said(b,nlower(a,b))). end_of_list. new given clause: 21 TRUE(Said(a,lower(a,b))). ** KEPT: 23 (21,8) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(norm(a)). ** KEPT: 24 (21,7,11) TRUE(atr(a)) | TRUE(norm(a)) | TRUE(nlower(a,b)). new given clause: 22 TRUE(Said(b,nlower(a,b))). ** KEPT: 25 (22,8) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(norm(b)). ** KEPT: 26 (22,7,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(lower(a,b)). new given clause: 23 (21,8) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(norm(a)). ** KEPT: 27 (23,17,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). ** KEPT: 28 (23,16,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(atr(b)) | TRUE(liar(b)). ** KEPT: 29 (23,15,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(liar(b)) | TRUE(norm(b)). ** KEPT: 30 (23,14,1) TRUE(liar(a)) | TRUE(norm(a)). ** KEPT: 31 (23,19,11) TRUE(lower(a,b)) | TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 32 (23,17,11) TRUE(lower(a,b)) | TRUE(norm(a)) | TRUE(nlower(x,a)). ** KEPT: 33 (23,12,11) TRUE(lower(a,b)) | TRUE(norm(a)) | TRUE(norm(x)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 34 (23,20,11) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 35 (23,16,11) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(liar(x)) | TRUE(nlower(x,a)). ** KEPT: 36 (23,13,11) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 30 back subsumes: 29 (23,15,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(liar(b)) | TRUE(norm(b)). 30 back subsumes: 28 (23,16,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(atr(b)) | TRUE(liar(b)). 30 back subsumes: 27 (23,17,1) TRUE(liar(a)) | TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). 30 back subsumes: 23 (21,8) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(norm(a)). new given clause: 30 (23,14,1) TRUE(liar(a)) | TRUE(norm(a)). ** KEPT: 37 (30,19,11) TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 38 (30,17,11) TRUE(norm(a)) | TRUE(nlower(x,a)). ** KEPT: 39 (30,12,11) TRUE(norm(a)) | TRUE(norm(x)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 40 (30,6,21,11) TRUE(norm(a)) | TRUE(nlower(a,b)). ** KEPT: 41 (30,20,11) TRUE(liar(a)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 42 (30,16,11) TRUE(liar(a)) | TRUE(liar(x)) | TRUE(nlower(x,a)). ** KEPT: 43 (30,13,11) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 37 back subsumes: 31 (23,19,11) TRUE(lower(a,b)) | TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 38 back subsumes: 32 (23,17,11) TRUE(lower(a,b)) | TRUE(norm(a)) | TRUE(nlower(x,a)). 39 back subsumes: 33 (23,12,11) TRUE(lower(a,b)) | TRUE(norm(a)) | TRUE(norm(x)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 40 back subsumes: 24 (21,7,11) TRUE(atr(a)) | TRUE(norm(a)) | TRUE(nlower(a,b)). 41 back subsumes: 34 (23,20,11) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 42 back subsumes: 35 (23,16,11) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(liar(x)) | TRUE(nlower(x,a)). 43 back subsumes: 36 (23,13,11) TRUE(lower(a,b)) | TRUE(liar(a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). new given clause: 38 (30,17,11) TRUE(norm(a)) | TRUE(nlower(x,a)). ** KEPT: 44 (38,20,11) TRUE(nlower(x,a)) | TRUE(norm(y)) | TRUE(lower(y,a)) | TRUE(lower(a,y)). ** KEPT: 45 (38,16,11) TRUE(nlower(x,a)) | TRUE(liar(y)) | TRUE(nlower(y,a)). ** KEPT: 46 (38,13,11) TRUE(nlower(x,a)) | TRUE(atr(y)) | TRUE(nlower(a,y)). ** KEPT: 47 (38,20,1) TRUE(norm(a)) | TRUE(lower(a,x)) | TRUE(atr(x)) | TRUE(liar(x)). ** KEPT: 48 (38,18,1) TRUE(norm(a)) | TRUE(atr(a)) | TRUE(lower(a,x)) | TRUE(liar(x)) | TRUE(norm(x)). 45 back subsumes: 42 (30,16,11) TRUE(liar(a)) | TRUE(liar(x)) | TRUE(nlower(x,a)). new given clause: 40 (30,6,21,11) TRUE(norm(a)) | TRUE(nlower(a,b)). ** KEPT: 49 (40,20,11) TRUE(nlower(a,b)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 50 (40,13,11) TRUE(nlower(a,b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 51 (40,19,30) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(lower(b,a)). ** KEPT: 52 (40,7,22) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). new given clause: 52 (40,7,22) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). ** KEPT: 53 (52,20,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 54 (52,13,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 55 (52,18,38) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(atr(a)) | TRUE(lower(a,b)). ** KEPT: 56 (52,18,11) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(atr(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 57 (52,15,11) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(norm(x)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 58 (52,14,11) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(nlower(b,x)). ** KEPT: 59 (52,20,38) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(lower(a,b)). ** KEPT: 60 (52,20,11) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 61 (52,16,11) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 62 (52,13,11) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). new given clause: 25 (22,8) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(norm(b)). ** KEPT: 63 (25,20,38) TRUE(liar(b)) | TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(nlower(x,a)). ** KEPT: 64 (25,20,30) TRUE(liar(b)) | TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(liar(a)). ** KEPT: 65 (25,19,11) TRUE(nlower(a,b)) | TRUE(norm(b)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 66 (25,17,11) TRUE(nlower(a,b)) | TRUE(norm(b)) | TRUE(nlower(x,b)). ** KEPT: 67 (25,20,11) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 68 (25,16,11) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 69 (25,13,11) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). 66 back subsumes: 65 (25,19,11) TRUE(nlower(a,b)) | TRUE(norm(b)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 66 back subsumes: 25 (22,8) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(norm(b)). new given clause: 26 (22,7,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(lower(a,b)). ** KEPT: 70 (26,18,11) TRUE(norm(b)) | TRUE(lower(a,b)) | TRUE(atr(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 71 (26,15,11) TRUE(norm(b)) | TRUE(lower(a,b)) | TRUE(norm(x)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 72 (26,14,11) TRUE(norm(b)) | TRUE(lower(a,b)) | TRUE(nlower(b,x)). ** KEPT: 73 (26,20,11) TRUE(atr(b)) | TRUE(lower(a,b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 74 (26,16,11) TRUE(atr(b)) | TRUE(lower(a,b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 75 (26,13,11) TRUE(atr(b)) | TRUE(lower(a,b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). ** KEPT: 76 (26,17,1) TRUE(atr(b)) | TRUE(norm(b)). 76 back subsumes: 54 (52,13,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 76 back subsumes: 53 (52,20,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 76 back subsumes: 52 (40,7,22) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(b)). 76 back subsumes: 26 (22,7,11) TRUE(atr(b)) | TRUE(norm(b)) | TRUE(lower(a,b)). new given clause: 76 (26,17,1) TRUE(atr(b)) | TRUE(norm(b)). ** KEPT: 77 (76,18,11) TRUE(norm(b)) | TRUE(atr(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 78 (76,15,11) TRUE(norm(b)) | TRUE(norm(x)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 79 (76,14,11) TRUE(norm(b)) | TRUE(nlower(b,x)). ** KEPT: 80 (76,20,11) TRUE(atr(b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 81 (76,16,11) TRUE(atr(b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 82 (76,13,11) TRUE(atr(b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). 77 back subsumes: 70 (26,18,11) TRUE(norm(b)) | TRUE(lower(a,b)) | TRUE(atr(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 77 back subsumes: 56 (52,18,11) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(atr(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 78 back subsumes: 71 (26,15,11) TRUE(norm(b)) | TRUE(lower(a,b)) | TRUE(norm(x)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 78 back subsumes: 57 (52,15,11) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(norm(x)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 79 back subsumes: 72 (26,14,11) TRUE(norm(b)) | TRUE(lower(a,b)) | TRUE(nlower(b,x)). 79 back subsumes: 58 (52,14,11) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(nlower(b,x)). 80 back subsumes: 73 (26,20,11) TRUE(atr(b)) | TRUE(lower(a,b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 80 back subsumes: 60 (52,20,11) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 81 back subsumes: 74 (26,16,11) TRUE(atr(b)) | TRUE(lower(a,b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 81 back subsumes: 61 (52,16,11) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 82 back subsumes: 75 (26,13,11) TRUE(atr(b)) | TRUE(lower(a,b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). 82 back subsumes: 62 (52,13,11) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). new given clause: 79 (76,14,11) TRUE(norm(b)) | TRUE(nlower(b,x)). ** KEPT: 83 (79,20,38) TRUE(nlower(b,x)) | TRUE(norm(a)) | TRUE(lower(a,b)). ** KEPT: 84 (79,20,11) TRUE(nlower(b,x)) | TRUE(norm(y)) | TRUE(lower(y,b)) | TRUE(lower(b,y)). ** KEPT: 85 (79,16,11) TRUE(nlower(b,x)) | TRUE(liar(y)) | TRUE(nlower(y,b)). ** KEPT: 86 (79,13,11) TRUE(nlower(b,x)) | TRUE(atr(y)) | TRUE(nlower(b,y)). ** KEPT: 87 (79,18,76) TRUE(norm(b)) | TRUE(atr(x)) | TRUE(lower(x,b)). 86 back subsumes: 82 (76,13,11) TRUE(atr(b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). 86 back subsumes: 69 (25,13,11) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(atr(x)) | TRUE(nlower(b,x)). 87 back subsumes: 77 (76,18,11) TRUE(norm(b)) | TRUE(atr(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 87 back subsumes: 55 (52,18,38) TRUE(norm(a)) | TRUE(norm(b)) | TRUE(atr(a)) | TRUE(lower(a,b)). new given clause: 43 (30,13,11) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 88 (43,19,11) TRUE(atr(x)) | TRUE(nlower(a,x)) | TRUE(liar(y)) | TRUE(lower(y,a)) | TRUE(lower(a,y)). ** KEPT: 89 (43,12,11) TRUE(atr(x)) | TRUE(nlower(a,x)) | TRUE(norm(y)) | TRUE(atr(y)) | TRUE(nlower(a,y)). ** KEPT: 90 (43,18,11) TRUE(liar(a)) | TRUE(nlower(a,x)) | TRUE(atr(y)) | TRUE(lower(y,x)) | TRUE(lower(x,y)). ** KEPT: 91 (43,15,11) TRUE(liar(a)) | TRUE(nlower(a,x)) | TRUE(norm(y)) | TRUE(liar(y)) | TRUE(nlower(y,x)). ** KEPT: 92 (43,14,11) TRUE(liar(a)) | TRUE(nlower(a,x)) | TRUE(nlower(x,y)). ** KEPT: 93 (43,5,22) TRUE(liar(a)) | TRUE(nlower(a,b)). ** KEPT: 94 (43,20,38) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(nlower(y,a)). ** KEPT: 95 (43,20,30) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(norm(x)) | TRUE(lower(x,a)). 89 back subsumes: 39 (30,12,11) TRUE(norm(a)) | TRUE(norm(x)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 95 back subsumes: 94 (43,20,38) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(nlower(y,a)). new given clause: 93 (43,5,22) TRUE(liar(a)) | TRUE(nlower(a,b)). ** KEPT: 96 (93,19,11) TRUE(nlower(a,b)) | TRUE(liar(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 97 (93,17,11) TRUE(nlower(a,b)) | TRUE(nlower(x,a)). ** KEPT: 98 (93,6,21,11) TRUE(nlower(a,b)). ** KEPT: 99 (93,20,38) TRUE(liar(a)) | TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(nlower(x,a)). ** KEPT: 100 (93,20,30) TRUE(liar(a)) | TRUE(norm(b)) | TRUE(lower(b,a)). 98 back subsumes: 97 (93,17,11) TRUE(nlower(a,b)) | TRUE(nlower(x,a)). 98 back subsumes: 96 (93,19,11) TRUE(nlower(a,b)) | TRUE(liar(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 98 back subsumes: 93 (43,5,22) TRUE(liar(a)) | TRUE(nlower(a,b)). 98 back subsumes: 68 (25,16,11) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 98 back subsumes: 67 (25,20,11) TRUE(nlower(a,b)) | TRUE(liar(b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 98 back subsumes: 66 (25,17,11) TRUE(nlower(a,b)) | TRUE(norm(b)) | TRUE(nlower(x,b)). 98 back subsumes: 50 (40,13,11) TRUE(nlower(a,b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 98 back subsumes: 49 (40,20,11) TRUE(nlower(a,b)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 98 back subsumes: 40 (30,6,21,11) TRUE(norm(a)) | TRUE(nlower(a,b)). 100 back subsumes: 99 (93,20,38) TRUE(liar(a)) | TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(nlower(x,a)). 100 back subsumes: 64 (25,20,30) TRUE(liar(b)) | TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(liar(a)). new given clause: 98 (93,6,21,11) TRUE(nlower(a,b)). ** KEPT: 101 (98,20,38) TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(nlower(x,a)). ** KEPT: 102 (98,19,43) TRUE(liar(b)) | TRUE(lower(b,a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 101 back subsumes: 63 (25,20,38) TRUE(liar(b)) | TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(nlower(x,a)). new given clause: 51 (40,19,30) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(lower(b,a)). ** KEPT: 103 (51,20,98) TRUE(liar(b)) | TRUE(lower(b,a)) | TRUE(norm(b)). ** KEPT: 104 (51,20,11) TRUE(liar(b)) | TRUE(lower(b,a)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 105 (51,19,79) TRUE(norm(a)) | TRUE(lower(b,a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(norm(b)). ** KEPT: 106 (51,19,11) TRUE(norm(a)) | TRUE(lower(b,a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 107 (51,17,11) TRUE(norm(a)) | TRUE(lower(b,a)) | TRUE(nlower(x,b)). ** KEPT: 108 (51,6,22,98) TRUE(norm(a)) | TRUE(lower(b,a)). ** KEPT: 109 (51,17,43) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 110 (51,17,30) TRUE(norm(a)) | TRUE(liar(b)). 108 back subsumes: 107 (51,17,11) TRUE(norm(a)) | TRUE(lower(b,a)) | TRUE(nlower(x,b)). 108 back subsumes: 106 (51,19,11) TRUE(norm(a)) | TRUE(lower(b,a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 108 back subsumes: 105 (51,19,79) TRUE(norm(a)) | TRUE(lower(b,a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(norm(b)). 108 back subsumes: 51 (40,19,30) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(lower(b,a)). 110 back subsumes: 109 (51,17,43) TRUE(norm(a)) | TRUE(liar(b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). new given clause: 110 (51,17,30) TRUE(norm(a)) | TRUE(liar(b)). ** KEPT: 111 (110,20,11) TRUE(liar(b)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 112 (110,13,11) TRUE(liar(b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 113 (110,19,79) TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(norm(b)). ** KEPT: 114 (110,19,11) TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 115 (110,17,11) TRUE(norm(a)) | TRUE(nlower(x,b)). ** KEPT: 116 (110,6,22,98) TRUE(norm(a)). 111 back subsumes: 104 (51,20,11) TRUE(liar(b)) | TRUE(lower(b,a)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 112 back subsumes: 102 (98,19,43) TRUE(liar(b)) | TRUE(lower(b,a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 116 back subsumes: 115 (110,17,11) TRUE(norm(a)) | TRUE(nlower(x,b)). 116 back subsumes: 114 (110,19,11) TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 116 back subsumes: 113 (110,19,79) TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,b)) | TRUE(norm(b)). 116 back subsumes: 110 (51,17,30) TRUE(norm(a)) | TRUE(liar(b)). 116 back subsumes: 108 (51,6,22,98) TRUE(norm(a)) | TRUE(lower(b,a)). 116 back subsumes: 83 (79,20,38) TRUE(nlower(b,x)) | TRUE(norm(a)) | TRUE(lower(a,b)). 116 back subsumes: 59 (52,20,38) TRUE(norm(a)) | TRUE(atr(b)) | TRUE(lower(a,b)). 116 back subsumes: 48 (38,18,1) TRUE(norm(a)) | TRUE(atr(a)) | TRUE(lower(a,x)) | TRUE(liar(x)) | TRUE(norm(x)). 116 back subsumes: 47 (38,20,1) TRUE(norm(a)) | TRUE(lower(a,x)) | TRUE(atr(x)) | TRUE(liar(x)). 116 back subsumes: 38 (30,17,11) TRUE(norm(a)) | TRUE(nlower(x,a)). 116 back subsumes: 37 (30,19,11) TRUE(norm(a)) | TRUE(liar(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 116 back subsumes: 30 (23,14,1) TRUE(liar(a)) | TRUE(norm(a)). new given clause: 116 (110,6,22,98) TRUE(norm(a)). ** KEPT: 117 (116,20,98) TRUE(norm(b)) | TRUE(lower(b,a)). ** KEPT: 118 (116,20,11) TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). ** KEPT: 119 (116,13,11) TRUE(atr(x)) | TRUE(nlower(a,x)). 117 back subsumes: 103 (51,20,98) TRUE(liar(b)) | TRUE(lower(b,a)) | TRUE(norm(b)). 117 back subsumes: 101 (98,20,38) TRUE(norm(b)) | TRUE(lower(b,a)) | TRUE(nlower(x,a)). 117 back subsumes: 100 (93,20,30) TRUE(liar(a)) | TRUE(norm(b)) | TRUE(lower(b,a)). 118 back subsumes: 111 (110,20,11) TRUE(liar(b)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 118 back subsumes: 44 (38,20,11) TRUE(nlower(x,a)) | TRUE(norm(y)) | TRUE(lower(y,a)) | TRUE(lower(a,y)). 118 back subsumes: 41 (30,20,11) TRUE(liar(a)) | TRUE(norm(x)) | TRUE(lower(x,a)) | TRUE(lower(a,x)). 119 back subsumes: 112 (110,13,11) TRUE(liar(b)) | TRUE(atr(x)) | TRUE(nlower(a,x)). 119 back subsumes: 89 (43,12,11) TRUE(atr(x)) | TRUE(nlower(a,x)) | TRUE(norm(y)) | TRUE(atr(y)) | TRUE(nlower(a,y)). 119 back subsumes: 88 (43,19,11) TRUE(atr(x)) | TRUE(nlower(a,x)) | TRUE(liar(y)) | TRUE(lower(y,a)) | TRUE(lower(a,y)). 119 back subsumes: 46 (38,13,11) TRUE(nlower(x,a)) | TRUE(atr(y)) | TRUE(nlower(a,y)). 119 back subsumes: 43 (30,13,11) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(nlower(a,x)). new given clause: 117 (116,20,98) TRUE(norm(b)) | TRUE(lower(b,a)). ** KEPT: 120 (117,20,11) TRUE(lower(b,a)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 121 (117,16,11) TRUE(lower(b,a)) | TRUE(liar(x)) | TRUE(nlower(x,b)). ** KEPT: 122 (117,16,116) TRUE(norm(b)) | TRUE(liar(b)). ** KEPT: 123 (117,14,76) TRUE(norm(b)). 123 back subsumes: 122 (117,16,116) TRUE(norm(b)) | TRUE(liar(b)). 123 back subsumes: 117 (116,20,98) TRUE(norm(b)) | TRUE(lower(b,a)). 123 back subsumes: 87 (79,18,76) TRUE(norm(b)) | TRUE(atr(x)) | TRUE(lower(x,b)). 123 back subsumes: 79 (76,14,11) TRUE(norm(b)) | TRUE(nlower(b,x)). 123 back subsumes: 78 (76,15,11) TRUE(norm(b)) | TRUE(norm(x)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 123 back subsumes: 76 (26,17,1) TRUE(atr(b)) | TRUE(norm(b)). new given clause: 123 (117,14,76) TRUE(norm(b)). ** KEPT: 124 (123,20,11) TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). ** KEPT: 125 (123,16,11) TRUE(liar(x)) | TRUE(nlower(x,b)). 124 back subsumes: 120 (117,20,11) TRUE(lower(b,a)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 124 back subsumes: 84 (79,20,11) TRUE(nlower(b,x)) | TRUE(norm(y)) | TRUE(lower(y,b)) | TRUE(lower(b,y)). 124 back subsumes: 80 (76,20,11) TRUE(atr(b)) | TRUE(norm(x)) | TRUE(lower(x,b)) | TRUE(lower(b,x)). 125 back subsumes: 121 (117,16,11) TRUE(lower(b,a)) | TRUE(liar(x)) | TRUE(nlower(x,b)). 125 back subsumes: 85 (79,16,11) TRUE(nlower(b,x)) | TRUE(liar(y)) | TRUE(nlower(y,b)). 125 back subsumes: 81 (76,16,11) TRUE(atr(b)) | TRUE(liar(x)) | TRUE(nlower(x,b)). new given clause: 119 (116,13,11) TRUE(atr(x)) | TRUE(nlower(a,x)). ** KEPT: 126 (119,18,11) TRUE(nlower(a,x)) | TRUE(atr(y)) | TRUE(lower(y,x)) | TRUE(lower(x,y)). ** KEPT: 127 (119,15,11) TRUE(nlower(a,x)) | TRUE(norm(y)) | TRUE(liar(y)) | TRUE(nlower(y,x)). ** KEPT: 128 (119,14,11) TRUE(nlower(a,x)) | TRUE(nlower(x,y)). ** KEPT: 129 (119,20,116) TRUE(atr(x)) | TRUE(norm(x)) | TRUE(lower(x,a)). 126 back subsumes: 90 (43,18,11) TRUE(liar(a)) | TRUE(nlower(a,x)) | TRUE(atr(y)) | TRUE(lower(y,x)) | TRUE(lower(x,y)). 127 back subsumes: 91 (43,15,11) TRUE(liar(a)) | TRUE(nlower(a,x)) | TRUE(norm(y)) | TRUE(liar(y)) | TRUE(nlower(y,x)). 128 back subsumes: 92 (43,14,11) TRUE(liar(a)) | TRUE(nlower(a,x)) | TRUE(nlower(x,y)). 129 back subsumes: 95 (43,20,30) TRUE(liar(a)) | TRUE(atr(x)) | TRUE(norm(x)) | TRUE(lower(x,a)). ------------ END OF SEARCH ------------ search stopped by max_given option. --------------- 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, 20). 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 22 clauses given 20 clauses generated 439 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 332 (clauses subsumed by sos) 180 unit deletions 0 clauses kept 107 empty clauses 0 factors generated 0 clauses back subsumed 94 clauses not processed 0 ----------- times (seconds) ----------- run time 6.06 input time 0.18 binary_res time 0.00 hyper_res time 1.22 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 3.58 demod time 0.00 weigh time 0.04 for_sub time 2.84 unit_del time 0.00 post_process time 0.98 back_sub time 0.48 conflict time 0.00 factor time 0.00 FPA build time 0.18 IS build time 0.06 print_cl time 0.46 cl integrate time 0.04 window time 0.00 SHAR_EOF # End of shell archive exit 0