% problem-set/geometry/tarski/t10.ver1.out % created : 07/21/89 % revised : 07/21/89 --------- OTTER 1.03+, 1989 --------- Job run on Fri Jul 21 03:53:43 1989 set(hyper_res). set(ur_res). set(order_eq). set(unit_deletion). 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) | EQUAL(x,y). 2 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 3 [] -B(x,y,z) | -B(x,y,v) | EQUAL(x,y) | B(x,z,v) | B(x,v,z). 4 [] L(x,y,y,x). 5 [] -L(x,y,z,z) | EQUAL(x,y). 6 [] -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). 7 [] -B(x,w,v) | -B(y,v,z) | B(x,op(w,x,y,z,v),y). 8 [] -B(x,w,v) | -B(y,v,z) | B(z,w,op(w,x,y,z,v)). 9 [] -L(x,y,x1,y1) | -L(y,z,y1,z1) | -L(x,v,x1,v1) | -L(y,v,y1,v1) | -B(x,y,z) | -B(x1,y1,z1) | EQUAL(x,y) | L(z,v,z1,v1). 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 [] EQUAL(x,x). 20 [] -EQUAL(x,y) | EQUAL(y,x). 21 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 22 [] -EQUAL(x,y) | -B(x,w,z) | B(y,w,z). 23 [] -EQUAL(x,y) | -B(w,x,z) | B(w,y,z). 24 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 25 [] -EQUAL(x,y) | -C(x,w,z) | C(y,w,z). 26 [] -EQUAL(x,y) | -C(w,x,z) | C(w,y,z). 27 [] -EQUAL(x,y) | -C(w,z,x) | C(w,z,y). 28 [] -EQUAL(x,y) | -L(x,v,w,z) | L(y,v,w,z). 29 [] -EQUAL(x,y) | -L(v,x,w,z) | L(v,y,w,z). 30 [] -EQUAL(x,y) | -L(v,w,x,z) | L(v,w,y,z). 31 [] -EQUAL(x,y) | -L(v,w,z,x) | L(v,w,y,z). 32 [] -EQUAL(x,y) | EQUAL(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)). 33 [] -EQUAL(x,y) | EQUAL(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)). 34 [] -EQUAL(x,y) | EQUAL(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)). 35 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)). 36 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)). 37 [] -EQUAL(x,y) | EQUAL(ext(x,v1,v2,v3),ext(y,v1,v2,v3)). 38 [] -EQUAL(x,y) | EQUAL(ext(v1,x,v2,v3),ext(v1,y,v2,v3)). 39 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,x,v3),ext(v1,v2,y,v3)). 40 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,v3,x),ext(v1,v2,v3,y)). 41 [] -B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z). end_of_list. list(sos). 42 [] B(x,x,y). 43 [] B(x,y,y). 44 [] C(a,b,c). 45 [] -C(a,c,b) | -C(b,a,c) | -C(b,c,a) | -C(c,a,b) | -C(c,b,a). end_of_list. list(demodulators). 46 [] EQUAL(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(c,0). end_of_list. ----> UNIT CONFLICT at 273.33 sec ----> 281 [binary,279,274] . ---------------- PROOF ---------------- 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). 41 [] -B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z). 42 [] B(x,x,y). 43 [] B(x,y,y). 44 [] C(a,b,c). 45 [] -C(a,c,b) | -C(b,a,c) | -C(b,c,a) | -C(c,a,b) | -C(c,b,a). 47 [hyper,44,15] B(a,b,c) | B(b,a,c) | B(a,c,b). 48 [hyper,47,18] B(b,a,c) | B(a,c,b) | C(a,c,b). 49 [hyper,47,17] B(b,a,c) | B(a,c,b) | C(b,a,c). 50 [hyper,47,18] B(a,b,c) | B(a,c,b) | C(b,c,a). 52 [hyper,47,17] B(a,b,c) | B(b,a,c) | C(c,a,b). 57 [hyper,48,16] B(b,a,c) | C(a,c,b). 61 [hyper,49,16] B(a,c,b) | C(b,a,c). 170 [hyper,43,41,42,61] B(b,c,a) | C(b,a,c). 171 [hyper,43,41,42,57] B(c,a,b) | C(a,c,b). 172 [hyper,43,41,42,52] B(c,a,b) | B(a,b,c) | C(c,a,b). 174 [hyper,43,41,42,50] B(b,c,a) | B(a,b,c) | C(b,c,a). 209 [hyper,170,18] C(b,a,c). 211 [hyper,171,17] C(a,c,b). 214 [hyper,172,16] B(a,b,c) | C(c,a,b). 218 [hyper,214,41,43,42] C(c,a,b) | B(c,b,a). 235 [hyper,218,18] C(c,a,b). 237 [hyper,174,16] B(a,b,c) | C(b,c,a). 241 [hyper,237,41,43,42] C(b,c,a) | B(c,b,a). 262 [hyper,241,17] C(b,c,a). 263 [ur,262,45,211,209,235] -C(c,b,a). 264 [ur,263,18] -B(c,a,b). 265 [ur,263,17] -B(b,c,a). 266 [ur,263,16] -B(c,b,a). 274 [ur,265,41,43,42] -B(a,c,b). 279 [ur,266,15,235,264] B(a,c,b). 281 [binary,279,274] . ------------ end of proof ------------- ------------- memory usage ------------ 5 mallocs of 32700 bytes each (159.7+ K) -------------- statistics ------------- clauses input 46 clauses given 91 clauses generated 13813 demod & eval rewrites 4 clauses wt or lit delete 6486 tautologies deleted 0 clauses forward subsumed 7038 (subsumed by sos) 1393 unit deletions 0 clauses kept 235 empty clauses 1 clauses back subsumed 144 clauses not processed 5 fpa argument overloads 38 fpa argument underloads 11 ----------- times (seconds) ----------- run time 273.54 (run time 0 hr, 4 min, 33 sec) input time 0.91 clausify time 0.00 hyper_res time 102.48 UR_res time 6.27 pre_process time 157.42 demod time 24.95 lex_rpo time 0.00 for_sub time 44.68 unit_del time 1.28 renumber time 8.35 cl integrate 0.28 print_cl time 1.04 post_process time 4.06 conflict time 0.18 back_sub time 1.68 FPA build time 0.64 IS build time 0.23 weigh cl time 52.42 window time 0.00