% problem-set/geometry/tarski/t2.ver1.out % created : 07/20/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 20 10:02:02 1989 set(ur_res). set(unit_deletion). assign(max_seconds,1800). assign(max_weight,50). list(axioms). 1 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 2 [] -B(x,y,z) | -B(x,y,v) | EQUAL(x,y) | B(x,z,v) | B(x,v,z). 3 [] -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). 4 [] -B(x,w,v) | -B(y,v,z) | B(x,op(w,x,y,z,v),y). 5 [] -B(x,w,v) | -B(y,v,z) | B(z,w,op(w,x,y,z,v)). 6 [] -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). 7 [] -B(C1,C2,C3). 8 [] -B(C2,C3,C1). 9 [] -B(C3,C1,C2). 10 [] EQUAL(x,x). 11 [] -EQUAL(x,y) | EQUAL(y,x). 12 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 13 [] -EQUAL(x,y) | -B(x,w,z) | B(y,w,z). 14 [] -EQUAL(x,y) | -B(w,x,z) | B(w,y,z). 15 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 16 [] -EQUAL(x,y) | -L(x,v,w,z) | L(y,v,w,z). 17 [] -EQUAL(x,y) | -L(v,x,w,z) | L(v,y,w,z). 18 [] -EQUAL(x,y) | -L(v,w,x,z) | L(v,w,y,z). 19 [] -EQUAL(x,y) | -L(v,w,z,x) | L(v,w,y,z). 20 [] -EQUAL(x,y) | EQUAL(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)). 21 [] -EQUAL(x,y) | EQUAL(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)). 22 [] -EQUAL(x,y) | EQUAL(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)). 23 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)). 24 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)). 25 [] -EQUAL(x,y) | EQUAL(ext(x,v1,v2,v3),ext(y,v1,v2,v3)). 26 [] -EQUAL(x,y) | EQUAL(ext(v1,x,v2,v3),ext(v1,y,v2,v3)). 27 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,x,v3),ext(v1,v2,y,v3)). 28 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,v3,x),ext(v1,v2,v3,y)). 29 [] -B(x,y,z) | B(z,y,x). end_of_list. list(sos). 30 [] -B(x,y,x) | EQUAL(x,y). 31 [] L(x,y,y,x). 32 [] -L(x,y,z,z) | EQUAL(x,y). 33 [] B(x,y,ext(x,y,w,v)). 34 [] L(y,ext(x,y,w,v),w,v). 35 [] -B(a,a,b). end_of_list. weight_list(purge_gen). weight(x,10). weight(C1,0). weight(C2,0). weight(C3,0). weight(a,0). weight(b,0). end_of_list. ----> UNIT CONFLICT at 9.95 sec ----> 89 [binary,87,34] . ---------------- PROOF ---------------- 11 [] -EQUAL(x,y) | EQUAL(y,x). 15 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 29 [] -B(x,y,z) | B(z,y,x). 32 [] -L(x,y,z,z) | EQUAL(x,y). 33 [] B(x,y,ext(x,y,w,v)). 34 [] L(y,ext(x,y,w,v),w,v). 35 [] -B(a,a,b). 36 [ur,35,29] -B(b,a,a). 38 [ur,33,15,36] -EQUAL(ext(b,a,x,y),a). 68 [ur,38,11] -EQUAL(a,ext(b,a,x,y)). 87 [ur,68,32] -L(a,ext(b,a,x,y),z,z). 89 [binary,87,34] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 35 clauses given 24 clauses generated 228 demod & eval rewrites 0 clauses wt or lit delete 42 tautologies deleted 0 clauses forward subsumed 133 (subsumed by sos) 11 unit deletions 0 clauses kept 54 empty clauses 1 clauses back subsumed 0 clauses not processed 3 fpa argument overloads 24 ----------- times (seconds) ----------- run time 10.09 (run time 0 hr, 0 min, 10 sec) input time 0.70 clausify time 0.00 UR_res time 7.71 pre_process time 1.19 demod time 0.00 lex_rpo time 0.00 for_sub time 0.53 unit_del time 0.00 renumber time 0.02 cl integrate 0.04 print_cl time 0.16 post_process time 0.25 conflict time 0.13 back_sub time 0.05 FPA build time 0.16 IS build time 0.06 weigh cl time 0.23 window time 0.00