problem-set/logic.problems/morgan/morgan.four.ver1.out created : 07/15/88 revised : 07/15/88 OTTER version 0.91, 14 June 1988. set(UR_res). list(axioms). 1 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 2 P(i(i(n(x1),n(x2)),i(x2,x1))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). end_of_list. list(sos). 5 P(i(x1,i(x2,x1))). 6 -P(i(n(n(a)),a)). end_of_list. ----> UNIT CONFLICT at 5.93 sec ----> 114 (113,85) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 P(i(i(x1,i(x2,x3)),i(i(x1,x2),i(x1,x3)))). 2 P(i(i(n(x1),n(x2)),i(x2,x1))). 3 -P(i(x1,x2)) | -P(x1) | P(x2). 4 -P(i(x1,x2)) | -P(i(x2,x3)) | P(i(x1,x3)). 5 P(i(x1,i(x2,x1))). 6 -P(i(n(n(a)),a)). 10 (5,4,2) P(i(n(x),i(x,y))). 12 (5,3,5) P(i(x,i(y,i(z,y)))). 13 (5,3,1) P(i(i(x,y),i(x,x))). 25 (10,4,6) -P(i(i(n(a),x),a)). 38 (25,4,2) -P(i(i(x,a),a)). 85 (12,3,38) -P(i(i(x,i(y,i(z,y))),i(i(u,a),a))). 105 (13,3,12) P(i(x,x)). 113 (105,3,1) P(i(i(i(x,y),x),i(i(x,y),y))). 114 (113,85) . --------------- 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). clear(order_eq). 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 6 clauses given 13 clauses generated 197 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 89 (clauses subsumed by sos) 32 unit deletions 0 clauses kept 108 empty clauses 1 factors generated 0 clauses back subsumed 4 clauses not processed 9 ----------- times (seconds) ----------- run time 6.17 input time 0.27 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.95 para_into time 0.00 para_from time 0.00 pre_process time 2.74 demod time 0.00 weigh time 0.06 for_sub time 0.89 unit_del time 0.00 post_process time 1.79 back_sub time 0.82 conflict time 0.82 factor time 0.00 FPA build time 0.20 IS build time 0.12 print_cl time 1.13 cl integrate time 0.32 window time 0.00