% problem-set/algebra/groups/order3.ver4.out % created : 08/15/88 % revised : 08/15/88 OTTER version 0.91, 14 June 1988. set(UR_res). set(back_demod). set(factor). set(Unit_deletion). assign(max_kept,5000). list(axioms). 1 -EL(x,xg) | -EL(y,xg) | P(xg,x,y,f(xg,x,y)). 2 -EL(x,xg) | -EL(y,xg) | EL(f(xg,x,y),xg). 3 -P(xg,x,y,z) | -P(xg,x,y,w) | EQUAL(w,z). 4 -P(xg,x,z,y) | -P(xg,x,w,y) | EQUAL(w,z). 5 -P(xg,z,y,x) | -P(xg,w,y,x) | EQUAL(w,z). 6 EL(e(xg),xg). 7 P(xg,e(xg),x,x). 8 P(xg,x,e(xg),x). 9 -EL(x,xg) | EL(g(xg,x),xg). 10 P(xg,g(xg,x),x,e(xg)). 11 P(xg,x,g(xg,x),e(xg)). 12 -P(xg,x,y,xy) | -P(xg,y,z,yz) | -P(xg,xy,z,xyz) | P(xg,x,xy,xyz). 13 -P(xg,x,y,xy) | -P(xg,y,z,yz) | -P(xg,x,yz,xyz) | P(xg,xy,z,xyz). 14 EQUAL(x,x). 15 -EQUAL(x,y) | EQUAL(y,x). 16 -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 17 -EQUAL(xg,yg) | -P(xg,x,y,z) | P(yg,x,y,z). 18 -EQUAL(x,y) | -P(xg,x,z,w) | P(xg,y,z,w). 19 -EQUAL(x,y) | -P(xg,w,x,z) | P(xg,w,y,z). 20 -EQUAL(x,y) | -P(xg,w,z,x) | P(xg,w,z,y). 21 -EQUAL(xg,yg) | EQUAL(f(xg,x,y),f(yg,x,y)). 22 -EQUAL(x,y) | EQUAL(f(xg,x,z),f(xg,y,z)). 23 -EQUAL(x,y) | EQUAL(f(xg,z,x),f(xg,z,y)). 24 -EQUAL(xg,yg) | EQUAL(g(xg,x),g(yg,x)). 25 -EQUAL(x,y) | EQUAL(g(xg,x),g(xg,y)). 26 -EQUAL(xg,yg) | -EL(x,xg) | EL(x,yg). 27 -EQUAL(x,y) | -EL(x,xg) | EL(y,xg). 28 -EQUAL(xg,yg) | EQUAL(e(xg),e(yg)). 29 -EQUAL(G1,G2). 30 EL(a,G1). 31 EL(b,G1). 32 EL(c,G1). 33 -EQUAL(a,b). 34 -EQUAL(c,a). 35 -EQUAL(b,c). 36 EL(d,G2). 37 EL(h,G2). 38 EL(j,G2). 39 -EQUAL(d,h). 40 -EQUAL(j,d). 41 -EQUAL(h,j). 42 -EL(x,G1) | EQUAL(x,a) | EQUAL(x,b) | EQUAL(x,c). 43 -EL(x,G2) | EQUAL(x,d) | EQUAL(x,h) | EQUAL(x,j). 44 EQUAL(e(G1),a). 45 EQUAL(e(G2),d). 46 P(G1,a,x,x). 47 P(G1,x,a,x). 48 P(G2,d,x,x). 49 P(G2,x,d,x). 50 EQUAL(p1(a),d). 51 EQUAL(p1(b),h). 52 EQUAL(p1(c),j). 53 EQUAL(p2(a),d). 54 EQUAL(p2(b),j). 55 EQUAL(p2(c),h). 56 EQUAL(p3(a),h). 57 EQUAL(p3(b),d). 58 EQUAL(p3(c),j). 59 EQUAL(q1(a),h). 60 EQUAL(q1(b),j). 61 EQUAL(q1(c),d). 62 EQUAL(q2(a),j). 63 EQUAL(q2(b),h). 64 EQUAL(q2(c),d). 65 EQUAL(q3(a),j). 66 EQUAL(q3(b),d). 67 EQUAL(q3(c),h). 68 -EQUAL(x,y) | EQUAL(p1(x),p1(y)). 69 -EQUAL(x,y) | EQUAL(p2(x),p2(y)). 70 -EQUAL(x,y) | EQUAL(p3(x),p3(y)). 71 -EQUAL(x,y) | EQUAL(q1(x),q1(y)). 72 -EQUAL(x,y) | EQUAL(q2(x),q2(y)). 73 -EQUAL(x,y) | EQUAL(q3(x),q3(y)). 74 -EQUAL(x,p1(z)) | -EQUAL(y,p1(z)) | EQUAL(x,y). 75 -EQUAL(x,p2(z)) | -EQUAL(y,p2(z)) | EQUAL(x,y). 76 -EQUAL(x,p3(z)) | -EQUAL(y,p3(z)) | EQUAL(x,y). 77 -EQUAL(x,q1(z)) | -EQUAL(y,q1(z)) | EQUAL(x,y). 78 -EQUAL(x,q2(z)) | -EQUAL(y,q2(z)) | EQUAL(x,y). 79 -EQUAL(x,q3(z)) | -EQUAL(y,q3(z)) | EQUAL(x,y). end_of_list. list(sos). 80 EL(d1,G1). 81 EL(d2,G1). 82 EL(d3,G1). 83 P(G1,d1,d2,d3). 84 -P(G1,p1(d1),p1(d2),p1(d3)) | -P(G1,p2(d1),p2(d2),p2(d3)) | -P(G1,p3(d1),p3(d2),p3(d3)) | -P(G1,q1(d1),q1(d2),q1(d3)) | -P(G2,q2(d1),q2(d2),q2(d3)) | -P(G3,q3(d1),q3(d2),q3(d3)). end_of_list. list(demodulators). 85 EQUAL(g(xg,e(xg)),e(xg)). 86 EQUAL(g(xg,g(xg,x)),x). 87 EQUAL(f(xg,e(xg),x),x). 88 EQUAL(f(xg,x,e(xg)),x). 89 EQUAL(f(xg,x,g(xg,x)),e(xg)). 90 EQUAL(f(xg,g(xg,x),x),e(xg)). 91 EQUAL(g(xg,f(xg,x,y)),f(xg,g(xg,x),g(xg,y))). 92 EQUAL(f(xg,x,f(xg,g(xg,x),y)),y). 93 EQUAL(f(xg,g(xg,x),f(xg,x,y)),y). 94 EQUAL(f(xg,f(xg,x,y),z),f(xg,x,f(xg,y,z))). 95 EQUAL(e(G1),a). 96 EQUAL(e(G2),d). 97 EQUAL(p1(a),d). 98 EQUAL(p1(b),h). 99 EQUAL(p1(c),j). 100 EQUAL(p2(a),d). 101 EQUAL(p2(b),j). 102 EQUAL(p2(c),h). 103 EQUAL(p3(a),h). 104 EQUAL(p3(b),d). 105 EQUAL(p3(c),j). 106 EQUAL(q1(a),h). 107 EQUAL(q1(b),j). 108 EQUAL(q1(c),d). 109 EQUAL(q2(a),j). 110 EQUAL(q2(b),h). 111 EQUAL(q2(c),d). 112 EQUAL(q3(a),j). 113 EQUAL(q3(b),d). 114 EQUAL(q3(c),h). end_of_list. new given clause: 80 EL(d1,G1). ------------> EMPTY CLAUSE -----------> 333 (311,12,46,46,47) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 4 -P(xg,x,z,y) | -P(xg,x,w,y) | EQUAL(w,z). 5 -P(xg,z,y,x) | -P(xg,w,y,x) | EQUAL(w,z). 12 -P(xg,x,y,xy) | -P(xg,y,z,yz) | -P(xg,xy,z,xyz) | P(xg,x,xy,xyz). 13 -P(xg,x,y,xy) | -P(xg,y,z,yz) | -P(xg,x,yz,xyz) | P(xg,xy,z,xyz). 33 -EQUAL(a,b). 46 P(G1,a,x,x). 47 P(G1,x,a,x). 83 P(G1,d1,d2,d3). 173 (83,12,47,46) P(G1,d1,d1,d3). 174 (83,12,46,83) P(G1,a,d1,d3). 275 (174,5,33) -P(G1,b,d1,d3). 276 (174,5,173) EQUAL(d1,a). 277 (276) EQUAL(d1,a). 279 (174,4,46,277) EQUAL(d3,a). 280 (279) EQUAL(d3,a). 306 (275,277,280) -P(G1,b,a,a). 311 (306,13,47,47) -P(G1,a,a,b). 333 (311,12,46,46,47) . --------------- options --------------- set(UR_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(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(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 114 clauses given 18 clauses generated 664 demodulation rewrites 770 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 612 (clauses subsumed by sos) 270 unit deletions 2 clauses kept 219 new demodualtors 4 empty clauses 1 factors generated 0 clauses back demodulated 167 clauses back subsumed 3 clauses not processed 5 ----------- times (seconds) ----------- run time 13.27 input time 1.45 binary_res time 0.00 hyper_res time 0.00 UR_res time 2.86 para_into time 0.00 para_from time 0.00 pre_process time 5.94 demod time 0.97 weigh time 0.07 for_sub time 2.17 unit_del time 0.55 post_process time 3.99 back_sub time 0.41 conflict time 0.80 factor time 0.03 back demod time 2.65 FPA build time 0.46 IS build time 0.19 print_cl time 1.66 cl integrate time 0.27 window time 0.00