% problem-set/geometry/tarski/t3.ver1.out % created : 07/20/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 20 10:02:12 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)). end_of_list. list(sos). 29 [] -B(x,y,x) | EQUAL(x,y). 30 [] L(x,y,y,x). 31 [] -L(x,y,z,z) | EQUAL(x,y). 32 [] B(x,y,ext(x,y,w,v)). 33 [] L(y,ext(x,y,w,v),w,v). 34 [] -B(a,b,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.79 sec ----> 81 [binary,79,33] . ---------------- PROOF ---------------- 11 [] -EQUAL(x,y) | EQUAL(y,x). 15 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 31 [] -L(x,y,z,z) | EQUAL(x,y). 32 [] B(x,y,ext(x,y,w,v)). 33 [] L(y,ext(x,y,w,v),w,v). 34 [] -B(a,b,b). 36 [ur,32,15,34] -EQUAL(ext(a,b,x,y),b). 63 [ur,36,11] -EQUAL(b,ext(a,b,x,y)). 79 [ur,63,31] -L(b,ext(a,b,x,y),z,z). 81 [binary,79,33] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 34 clauses given 22 clauses generated 206 demod & eval rewrites 0 clauses wt or lit delete 38 tautologies deleted 0 clauses forward subsumed 122 (subsumed by sos) 9 unit deletions 0 clauses kept 47 empty clauses 1 clauses back subsumed 0 clauses not processed 3 fpa argument overloads 24 ----------- times (seconds) ----------- run time 9.92 (run time 0 hr, 0 min, 9 sec) input time 0.70 clausify time 0.00 UR_res time 7.68 pre_process time 1.09 demod time 0.00 lex_rpo time 0.00 for_sub time 0.47 unit_del time 0.00 renumber time 0.02 cl integrate 0.04 print_cl time 0.14 post_process time 0.22 conflict time 0.12 back_sub time 0.05 FPA build time 0.18 IS build time 0.06 weigh cl time 0.22 window time 0.00