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). set(back_demod). assign(max_seconds,3600). 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_s(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 -el_s(0,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)) 95 eq_s(f4(xt),sigma(xt)). 96 eq_s(inter_s(x,y),inter_s(y,x)). 97 eq_c(inter_c(x,y),inter_c(y,x)). 98 eq_s(join_s(x,y),join_s(y,x)). 99 eq_c(join_c(x,y),join_c(y,x)). 100 eq_s(inter_s(inter_s(x,y),z),inter_s(x,inter_s(y,z))). 101 eq_c(inter_c(inter_c(x,y),z),inter_c(x,inter_c(y,z))). 102 eq_s(join_s(join_s(x,y),z),join_s(x,join_s(y,z))). 103 eq_c(join_c(join_c(x,y),z),join_c(x,join_c(y,z))). 104 eq_s(inter_s(x,x),x). 105 eq_s(inter_s(x,0),0). 106 eq_s(inter_s(0,x),0). 107 eq_s(join_s(x,x),x). 108 eq_s(join_s(x,0),x). 109 eq_s(join_s(0,x),x). 110 eq_s(inter_s(x,inter_s(x,y)),inter_s(x,y)). 111 eq_c(inter_c(x,inter_c(x,y)),inter_c(x,y)). 112 eq_s(inter_s(x,inter_s(y,x)),inter_s(x,y)). 113 eq_c(inter_c(x,inter_c(y,x)),inter_c(x,y)). 114 eq_s(join_s(x,join_s(x,y)),join_s(x,y)). 115 eq_c(join_c(x,join_c(x,y)),join_c(x,y)). 116 eq_s(join_s(x,join_s(y,x)),join_s(x,y)). 117 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 -----------> 123 (94,29,33) . ---------------- PROOF ---------------- 29 el_s(u,top_of_basis(xb)) | el_p(f10(xb,u),u). 33 -el_p(x,0). 94 -el_s(0,top_of_basis(B)). 123 (94,29,33) . ------------- memory usage ------------ 3 mallocs of 32700 bytes each (95.8+ K) -------------- statistics ------------- clauses input 117 clauses given 1 clauses generated 10 demodulation rewrites 1 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 1 (clauses subsumed by sos) 1 unit deletions 1 clauses kept 9 new demodualtors 0 empty clauses 1 factors generated 0 clauses back demodulated 0 clauses back subsumed 0 clauses not processed 0 fpa argument overloads 6 ----------- times (seconds) ----------- run time 2.45 input time 2.19 binary_res time 0.01 hyper_res time 0.00 ur_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.14 demod time 0.01 weigh time 0.02 for_sub time 0.04 unit_del time 0.02 post_process time 0.01 back_sub time 0.00 conflict time 0.00 factor time 0.00 back demod time 0.00 FPA build time 0.27 IS build time 0.08 print_cl time 0.34 cl integrate time 0.09 window time 0.00