problem-set/puzzles/miscell/barber.ver1.out created : 07/05/88 revised : 07/15/88 OTTER release 0.9, 19 May 1988 set(UR_res). list(axioms). 1 -MEMBER(x) | -MEMBER(y) | -SHAVED(x,y) | SHAVED(members,x). 2 -SHAVED(members,x) | -MEMBER(y) | SHAVED(y,x). 3 -SHAVED(Petruchio,Lorenzo) | ANSWER(Yes). end_of_list. list(sos). 4 MEMBER(Guido). 5 MEMBER(Lorenzo). 6 MEMBER(Petruchio). 7 MEMBER(Cesare). 8 SHAVED(Guido,Cesare). end_of_list. new given clause: 4 MEMBER(Guido). new given clause: 5 MEMBER(Lorenzo). new given clause: 6 MEMBER(Petruchio). new given clause: 7 MEMBER(Cesare). new given clause: 8 SHAVED(Guido,Cesare). ** KEPT: 9 (8,1,4,7) SHAVED(members,Guido). new given clause: 9 (8,1,4,7) SHAVED(members,Guido). ** KEPT: 10 (9,2,7) SHAVED(Cesare,Guido). ** KEPT: 11 (9,2,6) SHAVED(Petruchio,Guido). ** KEPT: 12 (9,2,5) SHAVED(Lorenzo,Guido). ** KEPT: 13 (9,2,4) SHAVED(Guido,Guido). new given clause: 10 (9,2,7) SHAVED(Cesare,Guido). ** KEPT: 14 (10,1,7,4) SHAVED(members,Cesare). new given clause: 11 (9,2,6) SHAVED(Petruchio,Guido). ** KEPT: 15 (11,1,6,4) SHAVED(members,Petruchio). new given clause: 12 (9,2,5) SHAVED(Lorenzo,Guido). ** KEPT: 16 (12,1,5,4) SHAVED(members,Lorenzo). new given clause: 13 (9,2,4) SHAVED(Guido,Guido). new given clause: 14 (10,1,7,4) SHAVED(members,Cesare). ** KEPT: 17 (14,2,7) SHAVED(Cesare,Cesare). ** KEPT: 18 (14,2,6) SHAVED(Petruchio,Cesare). ** KEPT: 19 (14,2,5) SHAVED(Lorenzo,Cesare). new given clause: 15 (11,1,6,4) SHAVED(members,Petruchio). ** KEPT: 20 (15,2,7) SHAVED(Cesare,Petruchio). ** KEPT: 21 (15,2,6) SHAVED(Petruchio,Petruchio). ** KEPT: 22 (15,2,5) SHAVED(Lorenzo,Petruchio). ** KEPT: 23 (15,2,4) SHAVED(Guido,Petruchio). new given clause: 16 (12,1,5,4) SHAVED(members,Lorenzo). ** KEPT: 24 (16,2,7) SHAVED(Cesare,Lorenzo). ** KEPT: 25 (16,2,6) SHAVED(Petruchio,Lorenzo). ** KEPT: 26 (16,2,5) SHAVED(Lorenzo,Lorenzo). ** KEPT: 27 (16,2,4) SHAVED(Guido,Lorenzo). new given clause: 17 (14,2,7) SHAVED(Cesare,Cesare). new given clause: 18 (14,2,6) SHAVED(Petruchio,Cesare). new given clause: 19 (14,2,5) SHAVED(Lorenzo,Cesare). new given clause: 20 (15,2,7) SHAVED(Cesare,Petruchio). new given clause: 21 (15,2,6) SHAVED(Petruchio,Petruchio). new given clause: 22 (15,2,5) SHAVED(Lorenzo,Petruchio). new given clause: 23 (15,2,4) SHAVED(Guido,Petruchio). new given clause: 24 (16,2,7) SHAVED(Cesare,Lorenzo). new given clause: 25 (16,2,6) SHAVED(Petruchio,Lorenzo). ** KEPT: 28 (25,3) ANSWER(Yes). 28 back subsumes: 3 -SHAVED(Petruchio,Lorenzo) | ANSWER(Yes). new given clause: 28 (25,3) ANSWER(Yes). new given clause: 26 (16,2,5) SHAVED(Lorenzo,Lorenzo). new given clause: 27 (16,2,4) SHAVED(Guido,Lorenzo). ------------ END OF SEARCH ------------ sos empty. --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 8 clauses given 25 clauses generated 33 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 13 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 20 empty clauses 0 factors generated 0 clauses back subsumed 1 clauses not processed 0 ----------- times (seconds) ----------- run time 0.64 input time 0.08 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.24 para_into time 0.00 para_from time 0.00 pre_process time 0.11 demod time 0.00 weigh time 0.00 for_sub time 0.02 unit_del time 0.00 post_process time 0.05 back_sub time 0.02 conflict time 0.02 factor time 0.00 FPA build time 0.03 IS build time 0.01 print_cl time 0.09 cl integrate time 0.01 window time 0.00