% problem-set/algebra/rings/index.ver1.out % created : 08/15/88 % revised : 08/15/88 OTTER version 0.91, 14 June 1988. set(hyper_res). set(back_demod). set(factor). set(Unit_deletion). assign(max_kept,5000). list(axioms). 1 P(e,x,x). 2 P(x,e,x). 3 P(g(x),x,e). 4 P(x,g(x),e). 5 P(x,y,f(x,y)). 6 -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 7 -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 8 -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). 9 -P(x,z,y) | -P(x,w,y) | EQUAL(z,w). 10 -P(z,y,x) | -P(w,y,x) | EQUAL(z,w). 11 EQUAL(x,x). 12 -EQUAL(x,y) | EQUAL(y,x). 13 -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 14 -EQUAL(x,y) | -P(x,w,z) | P(y,w,z). 15 -EQUAL(x,y) | -P(w,x,z) | P(w,y,z). 16 -EQUAL(x,y) | -P(w,z,x) | P(w,z,y). 17 -EQUAL(x,y) | EQUAL(f(x,w),f(y,w)). 18 -EQUAL(x,y) | EQUAL(f(w,x),f(w,y)). 19 -EQUAL(x,y) | EQUAL(g(x),g(y)). 20 O(e). 21 -O(x) | O(g(x)). 22 -O(x) | -O(y) | -P(x,y,z) | O(z). 23 O(x) | O(y) | O(l(x,y)). 24 O(x) | O(y) | P(x,l(x,y),y). 25 -EQUAL(x,y) | -O(x) | O(y). 26 -EQUAL(x,y) | EQUAL(l(w,x),l(w,y)). 27 -EQUAL(x,y) | EQUAL(l(x,w),l(y,w)). end_of_list. list(sos). 28 O(b). 29 P(b,g(a),c). 30 P(a,c,d). 31 -O(d). end_of_list. list(demodulators). 32 EQUAL(g(e),e). 33 EQUAL(f(x,e),x). 34 EQUAL(f(e,x),x). 35 EQUAL(f(x,g(x)),e). 36 EQUAL(f(g(x),x),e). 37 EQUAL(g(g(x)),x). 38 EQUAL(g(f(x,y)),f(g(x),g(y))). 39 EQUAL(f(x,f(g(x),y)),y). 40 EQUAL(f(g(x),f(x,y)),y). 41 EQUAL(f(f(x,y),z),f(x,f(y,z))). end_of_list. new given clause: 28 O(b). ------------> EMPTY CLAUSE -----------> 729 (31,722,28) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 4 P(x,g(x),e). 5 P(x,y,f(x,y)). 6 -P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w). 7 -P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w). 10 -P(z,y,x) | -P(w,y,x) | EQUAL(z,w). 28 O(b). 29 P(b,g(a),c). 30 P(a,c,d). 31 -O(d). 33 EQUAL(f(x,e),x). 37 EQUAL(g(g(x)),x). 38 EQUAL(g(f(x,y)),f(g(x),g(y))). 39 EQUAL(f(x,f(g(x),y)),y). 195 (29,7,4,5,37,33) P(c,a,b). 213 (195,7,30,5) P(d,a,f(a,b)). 716 (213,6,5,4,38,39) P(d,g(b),e). 721 (716,10,4) EQUAL(d,b). 722 (721) EQUAL(d,b). 729 (31,722,28) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(Unit_deletion). set(print_kept). set(factor). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). set(back_demod). set(print_new_demod). set(print_back_demod). 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(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). clear(dynamic_demod). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 5000). 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 41 clauses given 22 clauses generated 2159 demodulation rewrites 1313 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 1498 (clauses subsumed by sos) 328 unit deletions 29 clauses kept 1072 new demodualtors 10 empty clauses 1 factors generated 306 clauses back demodulated 411 clauses back subsumed 18 clauses not processed 426 ----------- times (seconds) ----------- run time 358.69 input time 0.50 binary_res time 0.00 hyper_res time 4.75 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 310.02 demod time 3.43 weigh time 0.50 for_sub time 290.61 unit_del time 2.58 post_process time 178.51 back_sub time 30.00 conflict time 0.37 factor time 32.99 back demod time 114.73 FPA build time 1.98 IS build time 1.01 print_cl time 6.05 cl integrate time 1.45 window time 0.00