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