problem-set/puzzles/miscell/jobs.ver1.out created : 07/12/88 revised : 07/12/88 OTTER version 0.9, 19 May 1988. set(UR_res). list(axioms). 1 eqp(x,x). 2 eqj(x,x). 3 -eqp(x,y) | eqp(y,x). 4 -eqj(x,y) | eqj(y,x). 5 -eqp(Roberta,Thelma). 6 -eqp(Roberta,Vince). 7 -eqp(Roberta,Steve). 8 -eqp(Vince,Thelma). 9 -eqp(Vince,Steve). 10 -eqj(CH,GU). 11 -eqj(CH,NU). 12 -eqj(CH,OP). 13 -eqj(CH,PO). 14 -eqj(CH,WA). 15 -eqj(CH,WR). 16 -eqj(CH,TE). 17 -eqj(GU,NU). 18 -eqj(GU,OP). 19 -eqj(GU,PO). 20 -eqj(GU,WA). 21 -eqj(GU,WR). 22 -eqj(GU,TE). 23 -eqj(NU,OP). 24 -eqj(NU,PO). 25 -eqj(NU,WA). 26 -eqj(NU,WR). 27 -eqj(NU,TE). 28 -eqj(OP,PO). 29 -eqj(OP,WA). 30 -eqj(OP,WR). 31 -eqj(OP,TE). 32 -eqj(PO,WA). 33 -eqj(PO,WR). 34 -eqj(PO,TE). 35 -eqj(WA,WR). 36 -eqj(WA,TE). 37 -eqj(WR,TE). 38 -hj(x,NU) | male(x). 39 -hj(x,WA) | male(x). 40 -hj(x,CH) | female(x). 41 -hj(x,NU) | educated(x). 42 -hj(x,TE) | educated(x). 43 -hj(x,PO) | educated(x). 44 -hj(x,CH) | -hj(x,PO). 45 -male(x) | -female(x). 46 male(x) | female(x). 47 -husb(x,y) | male(y). 48 -husb(x,y) | female(x). 49 -hj(x,CH) | -hj(y,OP) | husb(x,y). 50 -hj(x,CH) | hj(y,OP) | -husb(x,y). 51 -hj(x,z) | -hj(y,z) | eqp(x,y). 52 -hj(z,u) | -hj(z,x) | -hj(z,y) | eqj(u,x) | eqj(u,y) | eqj(x,y). 53 hj(Roberta,x) | hj(Thelma,x) | hj(Vince,x) | hj(Steve,x). 54 hj(x,CH) | hj(x,GU) | hj(x,NU) | hj(x,OP) | hj(x,PO) | hj(x,TE) | hj(x,WA) | hj(x,WR). 55 -hj(x1,CH) | -hj(x2,GU) | -hj(x3,NU) | -hj(x4,OP) | -hj(x5,PO) | -hj(x6,TE) | -hj(x7,WA) | -hj(x8,WR) | $ANS(CHEF(x1),GUARD(x2),NURSE(x3),OPERATOR(x4),POLICE(x5),TEACHER(x6),ACTOR(x7),BOXER(x8)). end_of_list. list(sos). 56 -educated(Vince). 57 -hj(Roberta,CH). 58 -hj(Roberta,WR). 59 -hj(Roberta,PO). 60 male(Steve). 61 male(Vince). 62 female(Roberta). 63 female(Thelma). end_of_list. ---------------- PROOF ---------------- 10 -eqj(CH,GU). 15 -eqj(CH,WR). 16 -eqj(CH,TE). 17 -eqj(GU,NU). 18 -eqj(GU,OP). 19 -eqj(GU,PO). 20 -eqj(GU,WA). 21 -eqj(GU,WR). 23 -eqj(NU,OP). 24 -eqj(NU,PO). 25 -eqj(NU,WA). 26 -eqj(NU,WR). 27 -eqj(NU,TE). 28 -eqj(OP,PO). 29 -eqj(OP,WA). 30 -eqj(OP,WR). 32 -eqj(PO,WA). 33 -eqj(PO,WR). 34 -eqj(PO,TE). 35 -eqj(WA,WR). 37 -eqj(WR,TE). 38 -hj(x,NU) | male(x). 39 -hj(x,WA) | male(x). 40 -hj(x,CH) | female(x). 41 -hj(x,NU) | educated(x). 42 -hj(x,TE) | educated(x). 43 -hj(x,PO) | educated(x). 44 -hj(x,CH) | -hj(x,PO). 45 -male(x) | -female(x). 47 -husb(x,y) | male(y). 49 -hj(x,CH) | -hj(y,OP) | husb(x,y). 52 -hj(z,u) | -hj(z,x) | -hj(z,y) | eqj(u,x) | eqj(u,y) | eqj(x,y). 53 hj(Roberta,x) | hj(Thelma,x) | hj(Vince,x) | hj(Steve,x). 55 -hj(x1,CH) | -hj(x2,GU) | -hj(x3,NU) | -hj(x4,OP) | -hj(x5,PO) | -hj(x6,TE) | -hj(x7,WA) | -hj(x8,WR) | $ANS(CHEF(x1),GUARD(x2),NURSE(x3),OPERATOR(x4),POLICE(x5),TEACHER(x6),ACTOR(x7),BOXER(x8)). 56 -educated(Vince). 57 -hj(Roberta,CH). 58 -hj(Roberta,WR). 59 -hj(Roberta,PO). 60 male(Steve). 61 male(Vince). 62 female(Roberta). 63 female(Thelma). 64 (56,43) -hj(Vince,PO). 65 (56,42) -hj(Vince,TE). 66 (56,41) -hj(Vince,NU). 67 (60,45) -female(Steve). 68 (61,45) -female(Vince). 69 (62,45) -male(Roberta). 70 (63,45) -male(Thelma). 72 (67,40) -hj(Steve,CH). 74 (68,40) -hj(Vince,CH). 75 (69,47) -husb(x,Roberta). 76 (69,39) -hj(Roberta,WA). 77 (69,38) -hj(Roberta,NU). 78 (70,47) -husb(x,Thelma). 79 (70,39) -hj(Thelma,WA). 80 (70,38) -hj(Thelma,NU). 81 (74,53,57,72) hj(Thelma,CH). 82 (80,53,77,66) hj(Steve,NU). 83 (81,49,78) -hj(Thelma,OP). 84 (81,49,75) -hj(Roberta,OP). 85 (81,44) -hj(Thelma,PO). 87 (85,53,59,64) hj(Steve,PO). 88 (87,52,82,17,19,24) -hj(Steve,GU). 89 (87,52,82,23,24,28) -hj(Steve,OP). 90 (87,52,82,24,27,34) -hj(Steve,TE). 91 (87,52,82,24,26,33) -hj(Steve,WR). 92 (87,52,82,24,25,32) -hj(Steve,WA). 93 (89,53,84,83) hj(Vince,OP). 95 (92,53,76,79) hj(Vince,WA). 97 (95,52,93,18,20,29) -hj(Vince,GU). 98 (95,52,93,29,30,35) -hj(Vince,WR). 99 (98,53,58,91) hj(Thelma,WR). 100 (99,52,81,10,15,21) -hj(Thelma,GU). 101 (99,52,81,15,16,37) -hj(Thelma,TE). 102 (100,53,97,88) hj(Roberta,GU). 103 (101,53,65,90) hj(Roberta,TE). 104 (102,55,81,82,93,87,95,99) -hj(x,TE) | $ANS(CHEF(Thelma),GUARD(Roberta),NURSE(Steve),OPERATOR(Vince),POLICE(Steve),TEACHER(x),ACTOR(Vince),BOXER(Thelma)). 105 (104,103) $ANS(CHEF(Thelma),GUARD(Roberta),NURSE(Steve),OPERATOR(Vince),POLICE(Steve),TEACHER(Roberta),ACTOR(Vince),BOXER(Thelma)). --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 63 clauses given 47 clauses generated 108 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 66 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 42 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 3.50 input time 0.36 binary_res time 0.00 hyper_res time 0.00 UR_res time 2.52 para_into time 0.00 para_from time 0.00 pre_process time 0.34 demod time 0.00 weigh time 0.02 for_sub time 0.20 unit_del time 0.00 post_process time 0.06 back_sub time 0.00 conflict time 0.04 factor time 0.00 FPA build time 0.08 IS build time 0.02 print_cl time 0.18 cl integrate time 0.02 window time 0.00