problem-set/puzzles/birds/bird1.ver1.out created : 08/11/88 revised : 08/11/88 OTTER version 0.91, 14 June 1988. set(para_from). set(para_into). set(para_from_left). set(para_from_right). list(axioms). 1 EQUAL(response(Mock,y),response(y,y)). 2 EQUAL(x,x). 3 EQUAL(response(comp(x,y),w),response(x,response(y,w))). end_of_list. list(sos). 4 -EQUAL(response(A,y),y). end_of_list. ---------------- PROOF ---------------- 1 EQUAL(response(Mock,y),response(y,y)). 2 EQUAL(x,x). 3 EQUAL(response(comp(x,y),w),response(x,response(y,w))). 4 -EQUAL(response(A,y),y). 5 (3,4) -EQUAL(response(comp(A,x),y),response(x,y)). 8 (1,5) -EQUAL(response(Mock,comp(A,x)),response(x,comp(A,x))). 13 (8,2) . --------------- options --------------- set(para_from). set(para_into). set(para_from_left). set(para_from_right). 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(UR_res). clear(demod_inf). 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 4 clauses given 3 clauses generated 11 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 2 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 9 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.29 input time 0.08 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.00 para_into time 0.02 para_from time 0.00 pre_process time 0.07 demod time 0.00 weigh time 0.00 for_sub time 0.00 unit_del time 0.00 post_process time 0.01 back_sub time 0.00 conflict time 0.01 factor time 0.00 FPA build time 0.03 IS build time 0.01 print_cl time 0.05 cl integrate time 0.01 window time 0.00