OTTER version 0.91, 14 June 1988. lex(0,X,U,V,B,sigma(x),f1(x,x),f2(x,x),f3(x,x),f4(x),f5(x,x,x,x,x),f6(x,x),f7(x,x),f8(x,x),f9(x,x,x),f10(x,x),g1(x,x),g2(x,x),g3(x,x),g4(x,x),inter_s(x,x)). set(ur_res). set(binary_res). set(unit_deletion). set(factor). assign(max_seconds,1800). assign(max_literals,10). list(axioms). 1 -top_space(x,xt) | el_s(0,xt). 2 -top_space(x,xt) | el_s(x,xt). 3 -top_space(x,xt) | -el_s(y,xt) | -el_s(w,xt) | el_s(inter_s(y,w),xt). 4 -top_space(x,xt) | -subset_s(z,xt) | el_s(sigma(z),xt). 5 top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | subset_s(f3(x,xt),xt). 6 top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f1(x,xt),xt) | -el_s(sigma(f3(x,xt)),xt). 7 top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | subset_s(f3(x,xt),xt). 8 top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | el_s(f2(x,xt),xt) | -el_s(sigma(f3(x,xt)),xt). 9 top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | -el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | subset_s(f3(x,xt),xt). 10 top_space(x,xt) | -el_s(0,xt) | -el_s(x,xt) | -el_s(inter_s(f1(x,xt),f2(x,xt)),xt) | -el_s(sigma(f3(x,xt)),xt). 11 -topology(xt) | top_space(f4(xt),xt). 12 topology(xt) | -top_space(uu4,xt). 13 eq_s(f4(xt),sigma(xt)). 14 -open(u,x,xt) | top_space(x,xt). 15 -open(u,x,xt) | el_s(u,xt). 16 open(u,x,xt) | -top_space(x,xt) | -el_s(u,xt). 17 -basis(xb,x) | eq_s(sigma(xb),x). 18 -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | el_p(f5(xb,x,xx,xb1,xb2),xb). 19 -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | el_p(xx,f5(xb,x,xx,xb1,xb2)). 20 -basis(xb,x) | -el_p(xx,x) | -el_s(xb1,xb) | -el_s(xb2,xb) | -el_p(xx,inter_s(xb1,xb2)) | subset_s(f5(xb,x,xx,xb1,xb2),inter_s(xb1,xb2)). 21 basis(xb,x) | -eq_s(sigma(xb),x) | el_p(f6(xb,x),x). 22 basis(xb,x) | -eq_s(sigma(xb),x) | el_s(f7(xb,x),xb). 23 basis(xb,x) | -eq_s(sigma(xb),x) | el_s(f8(xb,x),xb). 24 basis(xb,x) | -eq_s(sigma(xb),x) | el_p(f6(xb,x),inter_s(f7(xb,x),f8(xb,x))). 25 basis(xb,x) | -eq_s(sigma(xb),x) | -el_p(uu8,xb) | -el_p(f6(xb,x),uu8) | -subset_s(uu8,inter_s(f7(xb,x),f8(xb,x))). 26 -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_s(f9(xb,u,x),xb). 27 -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_p(x,f9(xb,u,x)). 28 -el_s(u,top_of_basis(xb)) | -el_p(x,u) | subset_s(f9(xb,u,x),u). 29 el_s(u,top_of_basis(xb)) | el_p(f10(xb,u),u). 30 el_s(u,top_of_basis(xb)) | -el_s(uu10,xb) | -el_p(f10(xb,u),uu10) | -subset_s(uu10,u). 31 subset_s(0,x). 32 -el_s(x,0). 33 -el_p(x,0). 34 subset_s(x,x). 35 subset_c(x,x). 36 -subset_s(x,y) | -subset_s(y,z) | subset_s(x,z). 37 -subset_c(x,y) | -subset_c(y,z) | subset_c(x,z). 38 -el_p(z,sigma(x)) | el_s(g1(z,x),x). 39 -el_p(z,sigma(x)) | el_p(z,g1(z,x)). 40 el_p(z,sigma(x)) | -el_s(uu1,x) | -el_p(z,uu1). 41 -el_s(x,y) | subset_s(x,sigma(y)). 42 -subset_s(x,y) | -el_s(y,z) | subset_s(x,sigma(z)). 43 -subset_s(x,y) | -el_p(u,x) | el_p(u,y). 44 subset_s(x,y) | el_p(g3(x,y),x). 45 subset_s(x,y) | -el_p(g3(x,y),y). 46 -subset_c(x,y) | -el_s(u,x) | el_s(u,y). 47 subset_c(x,y) | el_s(g4(x,y),x). 48 subset_c(x,y) | -el_s(g4(x,y),y). 49 -el_p(z,inter_s(x,y)) | el_p(z,x). 50 -el_p(z,inter_s(x,y)) | el_p(z,y). 51 el_p(z,inter_s(x,y)) | -el_p(z,x) | -el_p(z,y). 52 -el_s(z,join_c(x,y)) | el_s(z,x) | el_s(z,y). 53 el_s(z,join_c(x,y)) | -el_s(z,x). 54 el_s(z,join_c(x,y)) | -el_s(z,y). 55 -el_p(z,join_s(x,y)) | el_p(z,x) | el_p(z,y). 56 el_p(z,join_s(x,y)) | -el_p(z,x). 57 el_p(z,join_s(x,y)) | -el_p(z,y). 58 -subset_s(x1,y1) | -subset_s(x2,y2) | subset_s(inter_s(x1,x2),inter_s(y1,y2)). 59 eq_s(x,x). 60 eq_c(x,x). 61 eq_p(x,x). 62 -eq_s(x,y) | eq_s(y,x). 63 eq_s(x,y) | -eq_s(y,x). 64 -eq_s(x,y) | -eq_s(y,z) | eq_s(x,z). 65 -eq_c(x,y) | eq_c(y,x). 66 eq_c(x,y) | -eq_c(y,x). 67 -eq_c(x,y) | -eq_c(y,z) | eq_c(x,z). 68 -eq_p(x,y) | eq_p(y,x). 69 eq_p(x,y) | -eq_p(y,x). 70 -eq_p(x,y) | -eq_p(y,z) | eq_p(x,z). 71 -eq_c(x,y) | -subset_c(x,z) | subset_c(y,z). 72 -eq_s(x,y) | -subset_s(z,x) | subset_s(z,y). 73 -eq_s(x,y) | -top_space(x,z) | top_space(y,z). 74 -eq_c(x,y) | -top_space(z,x) | top_space(z,y). 75 -eq_c(x,y) | -topology(x) | topology(y). 76 -eq_s(x,y) | -el_s(x,z) | el_s(y,z). 77 -eq_s(x,y) | -el_p(z,x) | el_p(z,y). 78 -eq_c(x,y) | -el_s(z,x) | el_s(z,y). 79 -eq_s(x,y) | -open(x,z,w) | open(y,z,w). 80 -eq_s(x,y) | -open(z,x,w) | open(z,y,w). 81 -eq_c(x,y) | -open(w,z,x) | open(w,z,y). 82 -eq_c(x,y) | -basis(x,z) | basis(y,z). 83 -eq_s(x,y) | -basis(z,x) | basis(z,y). 84 -eq_s(x,y) | eq_s(inter_s(x,z),inter_s(y,z)). 85 eq_s(inter_s(x,y),inter_s(y,x)). 86 -eq_c(x,y) | eq_s(sigma(x),sigma(y)). 87 -eq_c(x,y) | eq_c(top_of_basis(x),top_of_basis(y)). 88 -eq_s(x,y) | subset_s(x,y). 89 -eq_s(x,y) | subset_s(y,x). 90 eq_s(x,y) | -subset_s(x,y) | -subset_s(y,x). 91 -eq_c(x,y) | subset_c(x,y). 92 -eq_c(x,y) | subset_c(y,x). 93 eq_c(x,y) | -subset_c(x,y) | -subset_c(y,x). end_of_list. list(sos). 94 subset_c(U,top_of_basis(B)). 95 -el_s(sigma(U),top_of_basis(B)). end_of_list. list(demodulators). lex-dependent demodulator: eq_s(inter_s(x,y),inter_s(y,x)) lex-dependent demodulator: eq_c(inter_c(x,y),inter_c(y,x)) lex-dependent demodulator: eq_s(join_s(x,y),join_s(y,x)) lex-dependent demodulator: eq_c(join_c(x,y),join_c(y,x)) 96 eq_s(f4(xt),sigma(xt)). 97 eq_s(inter_s(x,y),inter_s(y,x)). 98 eq_c(inter_c(x,y),inter_c(y,x)). 99 eq_s(join_s(x,y),join_s(y,x)). 100 eq_c(join_c(x,y),join_c(y,x)). 101 eq_s(inter_s(inter_s(x,y),z),inter_s(x,inter_s(y,z))). 102 eq_c(inter_c(inter_c(x,y),z),inter_c(x,inter_c(y,z))). 103 eq_s(join_s(join_s(x,y),z),join_s(x,join_s(y,z))). 104 eq_c(join_c(join_c(x,y),z),join_c(x,join_c(y,z))). 105 eq_s(inter_s(x,x),x). 106 eq_s(inter_s(x,0),0). 107 eq_s(inter_s(0,x),0). 108 eq_s(join_s(x,x),x). 109 eq_s(join_s(x,0),x). 110 eq_s(join_s(0,x),x). 111 eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)). 112 eq_c(inter_c(x,inter_c(x,y)),inter_c(x,y)). 113 eq_s(inter_s(x,inter_s(y,x)),inter_s(x,y)). 114 eq_c(inter_c(x,inter_c(y,x)),inter_c(x,y)). 115 eq_s(join_s(x,join_s(x,y)),join_s(x,y)). 116 eq_c(join_c(x,join_c(x,y)),join_c(x,y)). 117 eq_s(join_s(x,join_s(y,x)),join_s(x,y)). 118 eq_c(join_c(x,join_c(y,x)),join_c(x,y)). end_of_list. weight_list(pick_given). weight(f1(0,0),1). weight(f2(0,0),1). weight(f3(0,0),1). weight(f4(0),1). weight(f5(0,0,0,0,0),1). weight(f6(0,0),1). weight(f7(0,0),1). weight(f8(0,0),1). weight(f9(0,0,0),1). weight(f10(0,0),1). weight(g1(0,0),1). weight(g2(0,0),1). weight(g3(0,0),1). weight(g4(0,0),1). end_of_list. ------------> EMPTY CLAUSE -----------> 546 (454,30,95,457,502) . ---------------- PROOF ---------------- 26 -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_s(f9(xb,u,x),xb). 27 -el_s(u,top_of_basis(xb)) | -el_p(x,u) | el_p(x,f9(xb,u,x)). 28 -el_s(u,top_of_basis(xb)) | -el_p(x,u) | subset_s(f9(xb,u,x),u). 29 el_s(u,top_of_basis(xb)) | el_p(f10(xb,u),u). 30 el_s(u,top_of_basis(xb)) | -el_s(uu10,xb) | -el_p(f10(xb,u),uu10) | -subset_s(uu10,u). 38 -el_p(z,sigma(x)) | el_s(g1(z,x),x). 39 -el_p(z,sigma(x)) | el_p(z,g1(z,x)). 42 -subset_s(x,y) | -el_s(y,z) | subset_s(x,sigma(z)). 46 -subset_c(x,y) | -el_s(u,x) | el_s(u,y). 94 subset_c(U,top_of_basis(B)). 95 -el_s(sigma(U),top_of_basis(B)). 130 (95,29) el_p(f10(B,sigma(U)),sigma(U)). 142 (130,39) el_p(f10(B,sigma(U)),g1(f10(B,sigma(U)),U)). 143 (130,38) el_s(g1(f10(B,sigma(U)),U),U). 208 (143,46,94) el_s(g1(f10(B,sigma(U)),U),top_of_basis(B)). 451 (208,28,142) subset_s(f9(B,g1(f10(B,sigma(U)),U),f10(B,sigma(U))),g1(f10(B,sigma(U)),U)). 454 (208,27,142) el_p(f10(B,sigma(U)),f9(B,g1(f10(B,sigma(U)),U),f10(B,sigma(U)))). 457 (208,26,142) el_s(f9(B,g1(f10(B,sigma(U)),U),f10(B,sigma(U))),B). 502 (451,42,143) subset_s(f9(B,g1(f10(B,sigma(U)),U),f10(B,sigma(U))),sigma(U)). 546 (454,30,95,457,502) . ------------- memory usage ------------ 10 mallocs of 32700 bytes each (319.3+ K) -------------- statistics ------------- clauses input 118 clauses given 38 clauses generated 804 demodulation rewrites 170 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 369 (clauses subsumed by sos) 156 unit deletions 14 clauses kept 435 empty clauses 1 factors generated 48 clauses back subsumed 7 clauses not processed 13 fpa argument overloads 45 ----------- times (seconds) ----------- run time 31.89 input time 2.19 binary_res time 0.91 hyper_res time 0.00 ur_res time 4.59 para_into time 0.00 para_from time 0.00 pre_process time 20.73 demod time 1.38 weigh time 3.22 for_sub time 7.41 unit_del time 1.92 post_process time 6.31 back_sub time 1.81 conflict time 0.73 factor time 3.59 FPA build time 1.39 IS build time 0.67 print_cl time 3.58 cl integrate time 1.02 window time 0.00