#!/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 # interns.desc # interns.ver1.clauses # interns.ver1.in # interns.ver1.out # This archive created: Tue Aug 16 11:22:27 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/gen.test/README created : 07/26/88 revised : 07/26/88 Contents of 'gen.test' : ------------------------ Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/puzzles/gen.test. interns : To solve "The Interns Puzzle" ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a % and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in through OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background. SHAR_EOF if test -f 'interns.desc' then echo shar: over-writing existing file "'interns.desc'" fi cat << \SHAR_EOF > 'interns.desc' problem-set/puzzles/gen_test/interns.desc created : 07/27/88 revised : 07/27/88 Natural Language Description: The Interns Three interns are residents of the same hospital. On only one day of the week are all three interns on call. No intern is on call on three consecutive days. No two interns are off on the same day more than once a week. The first intern is off on Sunday, Tuesday, and Thursday. The second intern is off on Thursday and Saturday. The third intern is off on Sunday. Which day of the week are all three interns on call? Versions: interns.ver1.in- uses hyper-resolution. Has no denial. It terminates when the set of support becomes empty. created by : W. McCune verified for ITP : unverified translated for OTTER by : K.R. verified for OTTER : 07/27/88 SHAR_EOF if test -f 'interns.ver1.clauses' then echo shar: over-writing existing file "'interns.ver1.clauses'" fi cat << \SHAR_EOF > 'interns.ver1.clauses' % problem-set/puzzles/gen_test/interns.ver1.clauses % created : 07/27/88 % revised : 07/27/88 % description: % % This run solves "The Interns" puzzle using hyper-resolution. % % The Interns % % Three interns are residents of the same hospital. On only one % day of the week are all three interns on call. No intern is on % call on three consecutive days. No two interns are off on the % same day more than once a week. The first intern is off on % Sunday, Tuesday, and Thursday. The second intern is off on % Thursday and Saturday. The third intern is off on Sunday. % Which day of the week are all three interns on call? % representation: % % This version does has no denial. It terminates when sos becomes empty. % Definition of all_on (4 clauses). -all_on(x) | on(a,x). -all_on(x) | on(b,x). -all_on(x) | on(c,x). all_on(x) | -on(a,x) | -on(b,x) | -on(c,x). % All are on exactly one day of the week (2 clauses). % All are on at least one day of the week, and all are on at most % one day of the week. all_on(Sun) | all_on(Mon) | all_on(Tue) | all_on(Wed) | all_on(Thu) | all_on(Fri) | all_on(Sat). -all_on(x) | -all_on(y) | same_day(x,y). % No one is on for 3 consecutive days. -consec(x,y) | -consec(y,z) | -consec(z,w) | -on(u,x) | -on(u,y) | -on(u,z). % No 2 interns are off on the same day more than once a week. on(x,y) | on(x,z) | on(w,y) | on(w,z) | same_per(x,w) | same_day(y,z). % Definition of consecutive days. % (negative clauses omitted because there is nothing for them to resolve with) consec(Sun, Mon). consec(Mon, Tue). consec(Tue, Wed). consec(Wed, Thu). consec(Thu, Fri). consec(Fri, Sat). consec(Sat, Sun). % Definition of same_per and same_day. same_per(x,x). -same_per(a,b). -same_per(a,c). -same_per(b,c). same_day(x,x). -same_day(Sun, Mon). -same_day(Sun, Tue). -same_day(Sun, Wed). -same_day(Sun, Thu). -same_day(Sun, Fri). -same_day(Sun, Sat). -same_day(Mon, Tue). -same_day(Mon, Wed). -same_day(Mon, Thu). -same_day(Mon, Fri). -same_day(Mon, Sat). -same_day(Tue, Wed). -same_day(Tue, Thu). -same_day(Tue, Fri). -same_day(Tue, Sat). -same_day(Wed, Thu). -same_day(Wed, Fri). -same_day(Wed, Sat). -same_day(Thu, Fri). -same_day(Thu, Sat). -same_day(Fri, Sat). -on(a, Sun). -on(a, Tue). -on(a, Thu). -on(b, Thu). -on(b, Sat). -on(c, Sun). SHAR_EOF if test -f 'interns.ver1.in' then echo shar: over-writing existing file "'interns.ver1.in'" fi cat << \SHAR_EOF > 'interns.ver1.in' % problem-set/puzzles/gen_test/interns.ver1.in % created : 07/27/88 % revised : 07/27/88 % description: % % This run solves "The Interns" puzzle using hyper-resolution. % % The Interns % % Three interns are residents of the same hospital. On only one % day of the week are all three interns on call. No intern is on % call on three consecutive days. No two interns are off on the % same day more than once a week. The first intern is off on % Sunday, Tuesday, and Thursday. The second intern is off on % Thursday and Saturday. The third intern is off on Sunday. % Which day of the week are all three interns on call? % representation: % % This version does has no denial. It terminates when sos becomes empty. set(UR_res). list(axioms). % Definition of all_on (4 clauses). -all_on(x) | on(a,x). -all_on(x) | on(b,x). -all_on(x) | on(c,x). all_on(x) | -on(a,x) | -on(b,x) | -on(c,x). % All are on exactly one day of the week (2 clauses). % All are on at least one day of the week, and all are on at most % one day of the week. all_on(Sun) | all_on(Mon) | all_on(Tue) | all_on(Wed) | all_on(Thu) | all_on(Fri) | all_on(Sat). -all_on(x) | -all_on(y) | same_day(x,y). % No one is on for 3 consecutive days. -consec(x,y) | -consec(y,z) | -consec(z,w) | -on(u,x) | -on(u,y) | -on(u,z). % No 2 interns are off on the same day more than once a week. on(x,y) | on(x,z) | on(w,y) | on(w,z) | same_per(x,w) | same_day(y,z). % Definition of consecutive days. % (negative clauses omitted because there is nothing for them % to resolve with) consec(Sun, Mon). consec(Mon, Tue). consec(Tue, Wed). consec(Wed, Thu). consec(Thu, Fri). consec(Fri, Sat). consec(Sat, Sun). % Definition of same_per and same_day. same_per(x,x). -same_per(a,b). -same_per(a,c). -same_per(b,c). same_day(x,x). -same_day(Sun, Mon). -same_day(Sun, Tue). -same_day(Sun, Wed). -same_day(Sun, Thu). -same_day(Sun, Fri). -same_day(Sun, Sat). -same_day(Mon, Tue). -same_day(Mon, Wed). -same_day(Mon, Thu). -same_day(Mon, Fri). -same_day(Mon, Sat). -same_day(Tue, Wed). -same_day(Tue, Thu). -same_day(Tue, Fri). -same_day(Tue, Sat). -same_day(Wed, Thu). -same_day(Wed, Fri). -same_day(Wed, Sat). -same_day(Thu, Fri). -same_day(Thu, Sat). -same_day(Fri, Sat). end_of_list. list(sos). -on(a, Sun). -on(a, Tue). -on(a, Thu). -on(b, Thu). -on(b, Sat). -on(c, Sun). end_of_list. SHAR_EOF if test -f 'interns.ver1.out' then echo shar: over-writing existing file "'interns.ver1.out'" fi cat << \SHAR_EOF > 'interns.ver1.out' problem-set/puzzles/gen_test/interns.ver1.out created : 07/27/88 revised : 07/27/88 OTTER version 0.91, 14 June 1988. set(UR_res). list(axioms). 1 -all_on(x) | on(a,x). 2 -all_on(x) | on(b,x). 3 -all_on(x) | on(c,x). 4 all_on(x) | -on(a,x) | -on(b,x) | -on(c,x). 5 all_on(Sun) | all_on(Mon) | all_on(Tue) | all_on(Wed) | all_on(Thu) | all_on(Fri) | all_on(Sat). 6 -all_on(x) | -all_on(y) | same_day(x,y). 7 -consec(x,y) | -consec(y,z) | -consec(z,w) | -on(u,x) | -on(u,y) | -on(u,z). 8 on(x,y) | on(x,z) | on(w,y) | on(w,z) | same_per(x,w) | same_day(y,z). 9 consec(Sun,Mon). 10 consec(Mon,Tue). 11 consec(Tue,Wed). 12 consec(Wed,Thu). 13 consec(Thu,Fri). 14 consec(Fri,Sat). 15 consec(Sat,Sun). 16 same_per(x,x). 17 -same_per(a,b). 18 -same_per(a,c). 19 -same_per(b,c). 20 same_day(x,x). 21 -same_day(Sun,Mon). 22 -same_day(Sun,Tue). 23 -same_day(Sun,Wed). 24 -same_day(Sun,Thu). 25 -same_day(Sun,Fri). 26 -same_day(Sun,Sat). 27 -same_day(Mon,Tue). 28 -same_day(Mon,Wed). 29 -same_day(Mon,Thu). 30 -same_day(Mon,Fri). 31 -same_day(Mon,Sat). 32 -same_day(Tue,Wed). 33 -same_day(Tue,Thu). 34 -same_day(Tue,Fri). 35 -same_day(Tue,Sat). 36 -same_day(Wed,Thu). 37 -same_day(Wed,Fri). 38 -same_day(Wed,Sat). 39 -same_day(Thu,Fri). 40 -same_day(Thu,Sat). 41 -same_day(Fri,Sat). end_of_list. list(sos). 42 -on(a,Sun). 43 -on(a,Tue). 44 -on(a,Thu). 45 -on(b,Thu). 46 -on(b,Sat). 47 -on(c,Sun). end_of_list. new given clause: 42 -on(a,Sun). ** KEPT: 48 (42,1) -all_on(Sun). new given clause: 48 (42,1) -all_on(Sun). new given clause: 43 -on(a,Tue). ** KEPT: 49 (43,1) -all_on(Tue). new given clause: 49 (43,1) -all_on(Tue). new given clause: 44 -on(a,Thu). ** KEPT: 50 (44,1) -all_on(Thu). new given clause: 50 (44,1) -all_on(Thu). new given clause: 45 -on(b,Thu). ** KEPT: 51 (45,8,43,44,17,33) on(b,Tue). ** KEPT: 52 (45,8,42,44,17,24) on(b,Sun). new given clause: 46 -on(b,Sat). ** KEPT: 53 (46,8,44,45,17,40) on(a,Sat). ** KEPT: 54 (46,2) -all_on(Sat). new given clause: 54 (46,2) -all_on(Sat). new given clause: 47 -on(c,Sun). ** KEPT: 55 (47,8,42,44,18,24) on(c,Thu). ** KEPT: 56 (47,8,42,43,18,22) on(c,Tue). new given clause: 51 (45,8,43,44,17,33) on(b,Tue). new given clause: 52 (45,8,42,44,17,24) on(b,Sun). ** KEPT: 57 (52,7,9,10,11,51) -on(b,Mon). new given clause: 53 (46,8,44,45,17,40) on(a,Sat). new given clause: 55 (47,8,42,44,18,24) on(c,Thu). new given clause: 56 (47,8,42,43,18,22) on(c,Tue). ** KEPT: 58 (56,7,11,12,13,55) -on(c,Wed). new given clause: 57 (52,7,9,10,11,51) -on(b,Mon). ** KEPT: 59 (57,8,44,45,17,29) on(a,Mon). ** KEPT: 60 (57,2) -all_on(Mon). new given clause: 60 (57,2) -all_on(Mon). new given clause: 58 (56,7,11,12,13,55) -on(c,Wed). ** KEPT: 61 (58,8,42,47,18,23) on(a,Wed). ** KEPT: 62 (58,3) -all_on(Wed). new given clause: 62 (58,3) -all_on(Wed). ** KEPT: 63 (62,5,48,60,49,50,54) all_on(Fri). 63 back subsumes: 5 all_on(Sun) | all_on(Mon) | all_on(Tue) | all_on(Wed) | all_on(Thu) | all_on(Fri) | all_on(Sat). new given clause: 63 (62,5,48,60,49,50,54) all_on(Fri). ** KEPT: 64 (63,3) on(c,Fri). ** KEPT: 65 (63,2) on(b,Fri). ** KEPT: 66 (63,1) on(a,Fri). new given clause: 59 (57,8,44,45,17,29) on(a,Mon). new given clause: 61 (58,8,42,47,18,23) on(a,Wed). new given clause: 64 (63,3) on(c,Fri). ** KEPT: 67 (64,7,13,14,64,55) -consec(Fri,Thu). ** KEPT: 68 (64,7,13,14,56,55) -consec(Tue,Thu). ** KEPT: 69 (64,7,13,14,55,55) -consec(Thu,Thu). ** KEPT: 70 (64,7,13,14,55,64) -consec(Fri,Fri). ** KEPT: 71 (64,7,13,11,55,56) -consec(Fri,Tue). ** KEPT: 72 (64,7,13,14,15,55) -on(c,Sat). new given clause: 65 (63,2) on(b,Fri). new given clause: 66 (63,1) on(a,Fri). ** KEPT: 73 (66,7,14,14,66,53) -consec(Sat,Fri). ** KEPT: 74 (66,7,14,15,61,53) -consec(Wed,Fri). ** KEPT: 75 (66,7,14,15,59,53) -consec(Mon,Fri). ** KEPT: 76 (66,7,14,15,53,53) -consec(Sat,Sat). ** KEPT: 77 (66,7,14,12,53,61) -consec(Sat,Wed). ** KEPT: 78 (66,7,14,10,53,59) -consec(Sat,Mon). new given clause: 67 (64,7,13,14,64,55) -consec(Fri,Thu). new given clause: 68 (64,7,13,14,56,55) -consec(Tue,Thu). new given clause: 69 (64,7,13,14,55,55) -consec(Thu,Thu). new given clause: 70 (64,7,13,14,55,64) -consec(Fri,Fri). new given clause: 71 (64,7,13,11,55,56) -consec(Fri,Tue). new given clause: 72 (64,7,13,14,15,55) -on(c,Sat). ** KEPT: 79 (72,8,46,58,19,38) on(b,Wed). ** KEPT: 80 (72,8,57,46,19,31) on(c,Mon). new given clause: 73 (66,7,14,14,66,53) -consec(Sat,Fri). new given clause: 74 (66,7,14,15,61,53) -consec(Wed,Fri). new given clause: 75 (66,7,14,15,59,53) -consec(Mon,Fri). new given clause: 76 (66,7,14,15,53,53) -consec(Sat,Sat). new given clause: 77 (66,7,14,12,53,61) -consec(Sat,Wed). new given clause: 78 (66,7,14,10,53,59) -consec(Sat,Mon). new given clause: 79 (72,8,46,58,19,38) on(b,Wed). ** KEPT: 81 (79,7,11,12,79,51) -consec(Wed,Tue). ** KEPT: 82 (79,7,11,12,52,51) -consec(Sun,Tue). ** KEPT: 83 (79,7,11,12,51,51) -consec(Tue,Tue). ** KEPT: 84 (79,7,11,12,51,79) -consec(Wed,Wed). ** KEPT: 85 (79,7,11,9,51,52) -consec(Wed,Sun). new given clause: 80 (72,8,57,46,19,31) on(c,Mon). ** KEPT: 86 (80,7,13,10,55,64) -consec(Fri,Mon). ** KEPT: 87 (80,7,10,10,80,56) -consec(Tue,Mon). ** KEPT: 88 (80,7,10,11,80,56) -consec(Mon,Mon). ** KEPT: 89 (80,7,10,11,55,56) -consec(Thu,Mon). ** KEPT: 90 (80,7,13,14,55,64) -consec(Mon,Thu). ** KEPT: 91 (80,7,10,14,56,64) -consec(Tue,Fri). new given clause: 81 (79,7,11,12,79,51) -consec(Wed,Tue). new given clause: 82 (79,7,11,12,52,51) -consec(Sun,Tue). new given clause: 83 (79,7,11,12,51,51) -consec(Tue,Tue). new given clause: 84 (79,7,11,12,51,79) -consec(Wed,Wed). new given clause: 85 (79,7,11,9,51,52) -consec(Wed,Sun). new given clause: 86 (80,7,13,10,55,64) -consec(Fri,Mon). new given clause: 87 (80,7,10,10,80,56) -consec(Tue,Mon). new given clause: 88 (80,7,10,11,80,56) -consec(Mon,Mon). new given clause: 89 (80,7,10,11,55,56) -consec(Thu,Mon). new given clause: 90 (80,7,13,14,55,64) -consec(Mon,Thu). new given clause: 91 (80,7,10,14,56,64) -consec(Tue,Fri). ------------ END OF SEARCH ------------ sos empty. --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). set(print_new_demod). set(print_back_demod). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). clear(dynamic_demod). clear(back_demod). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 47 clauses given 50 clauses generated 116 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 72 (clauses subsumed by sos) 15 unit deletions 0 clauses kept 44 new demodualtors 0 empty clauses 0 factors generated 0 clauses back demodulated 0 clauses back subsumed 1 clauses not processed 0 ----------- times (seconds) ----------- run time 3.56 input time 0.22 binary_res time 0.00 hyper_res time 0.00 UR_res time 3.04 para_into time 0.00 para_from time 0.00 pre_process time 0.20 demod time 0.00 weigh time 0.00 for_sub time 0.14 unit_del time 0.00 post_process time 0.02 back_sub time 0.00 conflict time 0.02 factor time 0.00 back demod time 0.00 FPA build time 0.06 IS build time 0.00 print_cl time 0.06 cl integrate time 0.04 window time 0.00 SHAR_EOF # End of shell archive exit 0