% problem-set/geometry/tarski/t7.ver1.out % created : 07/20/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 20 10:02:26 1989 set(hyper_res). set(ur_res). set(order_eq). set(unit_deletion). assign(max_seconds,1800). set_skolem([ext(x,y,z,w),op(u,v,w,x,y),euc1(u,v,w,x,y),euc2(u,v,w,x,y),cont(u,v,w,x,y,z)]). 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 [] EQUAL(x,x). 16 [] -EQUAL(x,y) | EQUAL(y,x). 17 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 18 [] -EQUAL(x,y) | -B(x,w,z) | B(y,w,z). 19 [] -EQUAL(x,y) | -B(w,x,z) | B(w,y,z). 20 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 21 [] -EQUAL(x,y) | -L(x,v,w,z) | L(y,v,w,z). 22 [] -EQUAL(x,y) | -L(v,x,w,z) | L(v,y,w,z). 23 [] -EQUAL(x,y) | -L(v,w,x,z) | L(v,w,y,z). 24 [] -EQUAL(x,y) | -L(v,w,z,x) | L(v,w,y,z). 25 [] -EQUAL(x,y) | EQUAL(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)). 26 [] -EQUAL(x,y) | EQUAL(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)). 27 [] -EQUAL(x,y) | EQUAL(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)). 28 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)). 29 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)). 30 [] -EQUAL(x,y) | EQUAL(ext(x,v1,v2,v3),ext(y,v1,v2,v3)). 31 [] -EQUAL(x,y) | EQUAL(ext(v1,x,v2,v3),ext(v1,y,v2,v3)). 32 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,x,v3),ext(v1,v2,y,v3)). 33 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,v3,x),ext(v1,v2,v3,y)). 34 [] -B(x,y,z) | B(z,y,x). end_of_list. list(sos). 35 [] -EQUAL(a,c). 36 [] B(d,a,c). 37 [] B(e,a,c). 38 [] -B(d,e,a). 39 [] -B(e,d,a). end_of_list. weight_list(purge_gen). weight(x,20). end_of_list. ----> UNIT CONFLICT at 7.61 sec ----> 81 [binary,79,63] . ---------------- PROOF ---------------- 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). 15 [] EQUAL(x,x). 17 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 34 [] -B(x,y,z) | B(z,y,x). 35 [] -EQUAL(a,c). 36 [] B(d,a,c). 37 [] B(e,a,c). 38 [] -B(d,e,a). 39 [] -B(e,d,a). 40 [ur,35,17,15] -EQUAL(c,a). 43 [hyper,36,34] B(c,a,d). 45 [hyper,37,34] B(c,a,e). 48 [ur,38,2,37] -B(d,e,c). 50 [ur,39,2,36] -B(e,d,c). 60 [ur,48,34] -B(c,e,d). 63 [ur,50,34] -B(c,d,e). 79 [ur,60,3,43,45,40] B(c,d,e). 81 [binary,79,63] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 39 clauses given 25 clauses generated 265 demod & eval rewrites 0 clauses wt or lit delete 81 tautologies deleted 0 clauses forward subsumed 143 (subsumed by sos) 31 unit deletions 3 clauses kept 42 empty clauses 1 clauses back subsumed 0 clauses not processed 4 fpa argument overloads 28 ----------- times (seconds) ----------- run time 7.76 (run time 0 hr, 0 min, 7 sec) input time 0.77 clausify time 0.00 hyper_res time 0.49 UR_res time 4.84 pre_process time 1.21 demod time 0.00 lex_rpo time 0.00 for_sub time 0.59 unit_del time 0.02 renumber time 0.09 cl integrate 0.02 print_cl time 0.12 post_process time 0.22 conflict time 0.12 back_sub time 0.04 FPA build time 0.14 IS build time 0.04 weigh cl time 0.11 window time 0.00