% problem-set/geometry/tarski/t13.ver1.out % created : 07/28/89 % revised : 07/29/89 --------- OTTER 1.03+, 1989 --------- Job run on Sat Jul 29 15:30:04 1989 set(hyper_res). set(ur_res). set(order_eq). set(unit_deletion). assign(max_mem,2000). assign(max_seconds,2400). set_skolem([ext(x,y,z,w),op(u,v,w,x,y)]). set(delete_identical_nested_skolem). assign(max_weight,30). list(axioms). 1 [] -B(x,y,x) | EQ(x,y). 2 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 3 [] -B(x,y,z) | -B(x,y,v) | B(x,z,v) | B(x,v,z) | EQ(x,y). 4 [] L(x,y,y,x). 5 [] -L(x,y,z,z) | EQ(x,y). 6 [] -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). 7 [] B(x,op(w,x,y,z,v),y) | -B(x,w,v) | -B(y,v,z). 8 [] B(z,w,op(w,x,y,z,v)) | -B(x,w,v) | -B(y,v,z). 9 [] -L(x,y,x1,y1) | -L(y,z,y1,z1) | -L(x,v,x1,v1) | -L(y,v,y1,v1) | L(z,v,z1,v1) | -B(x,y,z) | -B(x1,y1,z1) | EQ(x,y). 10 [] B(x,y,ext(x,y,w,v)). 11 [] L(y,ext(x,y,w,v),w,v). 12 [] -B(C1,C2,C3). 13 [] -B(C2,C3,C1). 14 [] -B(C3,C1,C2). 15 [] -C(x,y,z) | B(x,y,z) | B(y,x,z) | B(x,z,y). 16 [] -B(x,y,z) | C(x,y,z). 17 [] -B(y,x,z) | C(x,y,z). 18 [] -B(x,z,y) | C(x,y,z). 19 [] EQ(x,x). 20 [] -EQ(x,y) | EQ(y,x). 21 [] -EQ(x,y) | -EQ(y,z) | EQ(x,z). 22 [] -B(x,w,z) | B(y,w,z) | -EQ(x,y). 23 [] -B(w,x,z) | B(w,y,z) | -EQ(x,y). 24 [] -B(w,z,x) | B(w,z,y) | -EQ(x,y). 25 [] -C(x,w,z) | C(y,w,z) | -EQ(x,y). 26 [] -C(w,x,z) | C(w,y,z) | -EQ(x,y). 27 [] -C(w,z,x) | C(w,z,y) | -EQ(x,y). 28 [] -L(x,v,w,z) | L(y,v,w,z) | -EQ(x,y). 29 [] -L(v,x,w,z) | L(v,y,w,z) | -EQ(x,y). 30 [] -L(v,w,x,z) | L(v,w,y,z) | -EQ(x,y). 31 [] -L(v,w,z,x) | L(v,w,y,z) | -EQ(x,y). 32 [] EQ(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)) | -EQ(x,y). 33 [] EQ(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)) | -EQ(x,y). 34 [] EQ(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)) | -EQ(x,y). 35 [] EQ(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)) | -EQ(x,y). 36 [] EQ(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)) | -EQ(x,y). 37 [] EQ(ext(x,v1,v2,v3),ext(y,v1,v2,v3)) | -EQ(x,y). 38 [] EQ(ext(v1,x,v2,v3),ext(v1,y,v2,v3)) | -EQ(x,y). 39 [] EQ(ext(v1,v2,x,v3),ext(v1,v2,y,v3)) | -EQ(x,y). 40 [] EQ(ext(v1,v2,v3,x),ext(v1,v2,v3,y)) | -EQ(x,y). 41 [] -B(x,y,z) | B(z,y,x). 42 [] B(x,x,y). 43 [] B(x,y,y). 44 [] -B(x,z,y) | -B(x,y,z) | EQ(x,y) | EQ(y,z) | EQ(x,z). 45 [] -B(y,x,z) | -B(x,y,z) | EQ(x,y) | EQ(y,z) | EQ(x,z). 46 [] -B(w,y,z) | -B(x,y,z) | B(x,w,y) | B(w,x,y) | EQ(y,z). 47 [] -B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z). 48 [] -C(x,y,z) | C(x,z,y). 49 [] -C(x,y,z) | C(y,x,z). 50 [] -C(x,y,z) | C(y,z,x). 51 [] -C(x,y,z) | C(z,x,y). 52 [] -C(x,y,z) | C(z,y,x). 53 [] -B(w,v,u) | C(u,v,w). 54 [] -B(u,w,v) | C(u,v,w). 55 [] -B(v,u,w) | C(u,v,w). 56 [] C(x,x,y). 57 [] C(x,y,x). 58 [] C(y,x,x). 59 [] C(x,z,y) | -EQ(x,y). 60 [] -L(u,v,u1,v1) | -L(v,w,v1,w1) | -L(u,w,u1,w1) | -C(u,v,w) | C(u1,v1,w1). 61 [] -C(w,v,u) | -C(x,v,u) | C(x,w,u) | EQ(u,v). 62 [] -C(w,v,u) | -C(x,v,u) | C(x,w,v) | EQ(u,v). 63 [] -C(u,v,w) | -C(u,v,x) | C(u,w,x) | EQ(u,v). 64 [] -C(u,v,w) | -C(u,v,x) | C(v,w,x) | EQ(u,v). end_of_list. list(sos). 65 [] -C(C1,C2,C3). 66 [] -EQ(a,b). 67 [] C(a,b,d1). 68 [] C(a,b,d2). 69 [] C(a,b,d3). 70 [] -C(d1,d2,d3). end_of_list. list(demodulators). 71 [] EQ(ext(x,y,z,z),y). end_of_list. weight_list(pick_and_purge). weight(x,20). weight(C1,0). weight(C2,0). weight(C3,0). weight(a,0). weight(b,0). weight(d1,0). weight(d2,0). weight(d3,0). end_of_list. -----> EMPTY CLAUSE at 28.38 sec ----> 175 [hyper,104,64,92,unit_del,70,174] . ---------------- PROOF ---------------- 19 [] EQ(x,x). 21 [] -EQ(x,y) | -EQ(y,z) | EQ(x,z). 25 [] -C(x,w,z) | C(y,w,z) | -EQ(x,y). 64 [] -C(u,v,w) | -C(u,v,x) | C(v,w,x) | EQ(u,v). 66 [] -EQ(a,b). 67 [] C(a,b,d1). 68 [] C(a,b,d2). 69 [] C(a,b,d3). 70 [] -C(d1,d2,d3). 83 [ur,66,21,19] -EQ(b,a). 92 [hyper,68,64,67,unit_del,83] C(b,d1,d2). 103 [hyper,69,64,68,unit_del,83] C(b,d2,d3). 104 [hyper,69,64,67,unit_del,83] C(b,d1,d3). 174 [ur,103,25,70] -EQ(d1,b). 175 [hyper,104,64,92,unit_del,70,174] . ------------ end of proof ------------- ------------- memory usage ------------ 3 mallocs of 32700 bytes each (95.8+ K) -------------- statistics ------------- clauses input 71 clauses given 35 clauses generated 1408 demod & eval rewrites 0 clauses wt or lit delete 25 tautologies deleted 0 clauses forward subsumed 1271 (subsumed by sos) 295 unit deletions 37 clauses kept 112 empty clauses 1 clauses back subsumed 12 clauses not processed 9 fpa argument overloads 24 ----------- times (seconds) ----------- run time 28.52 (run time 0 hr, 0 min, 28 sec) input time 1.29 clausify time 0.00 hyper_res time 1.91 UR_res time 15.11 pre_process time 9.11 demod time 0.72 lex_rpo time 0.00 for_sub time 4.34 unit_del time 0.44 renumber time 0.47 cl integrate 0.07 print_cl time 0.32 post_process time 0.65 conflict time 0.29 back_sub time 0.12 FPA build time 0.29 IS build time 0.11 weigh cl time 1.44 window time 0.00