% problem-set/geometry/tarski/t11.ver3.out % created : 07/25/89 % revised : 07/28/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 27 14:24:36 1989 set(hyper_res). set(order_eq). set(unit_deletion). assign(max_weight,40). assign(max_seconds,1800). assign(max_mem,1500). set_skolem([ext(x,y,z,w),ip(u,v,w,x,y)]). set(delete_identical_nested_skolem). list(axioms). 1 [] (x = x). 2 [] EQ(x,x). end_of_list. list(sos). 3 [] C(C1,C2,C3). 4 [] (dist(u,v) = dist(v,u)). 5 [] (dist(u,v) != dist(w,x)) | (dist(u,v) != dist(y,z)) | (dist(w,x) = dist(y,z)). 6 [] (dist(u,v) != dist(w,w)) | EQ(u,v). 7 [] B(u,v,ext(u,v,w,x)). 8 [] (dist(v,ext(u,v,w,x)) = dist(w,x)). 9 [] (dist(u,v) != dist(u1,v1)) | (dist(v,w) != dist(v1,w1)) | (dist(u,x) != dist(u1,x1)) | (dist(v,x) != dist(v1,x1)) | (dist(w,x) = dist(w1,x1)) | -B(u,v,w) | -B(u1,v1,w1) | EQ(u,v). 10 [] -B(u,v,u) | EQ(u,v). 11 [] B(v,ip(u,v,w,x,y),y) | -B(u,v,w) | -B(y,x,w). 12 [] B(x,ip(u,v,w,x,y),u) | -B(u,v,w) | -B(y,x,w). 13 [] -B(C1,C2,C3). 14 [] -B(C2,C3,C1). 15 [] -B(C3,C1,C2). 16 [] -B(u,v,w) | C(u,v,w). 17 [] -B(v,w,u) | C(u,v,w). 18 [] -B(w,u,v) | C(u,v,w). 19 [] -C(u,v,w) | B(u,v,w) | B(v,w,u) | B(w,u,v). 20 [] -B(u,v,w) | -B(u,v,x) | B(u,w,x) | B(u,x,w) | EQ(u,v). end_of_list. list(demodulators). 21 [] (dist(v,ext(u,v,w,x)) = dist(w,x)). 22 [] (ext(u,v,u,v) = R(u,v)). 23 [] (ext(ext(w1,u1,C1,C2),u1,u,v) = ins(u1,w1,u,v)). end_of_list. weight_list(pick_and_purge). weight(x,20). weight(C1,0). weight(C2,0). weight(C3,0). end_of_list. -----> EMPTY CLAUSE at 0.13 sec ----> 24 [hyper,19,3,unit_del,13,14,15] . ---------------- PROOF ---------------- 3 [] C(C1,C2,C3). 13 [] -B(C1,C2,C3). 14 [] -B(C2,C3,C1). 15 [] -B(C3,C1,C2). 19 [] -C(u,v,w) | B(u,v,w) | B(v,w,u) | B(w,u,v). 24 [hyper,19,3,unit_del,13,14,15] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 23 clauses given 13 clauses generated 7 demod & eval rewrites 0 clauses wt or lit delete 6 tautologies deleted 0 clauses forward subsumed 0 (subsumed by sos) 0 unit deletions 3 clauses kept 1 empty clauses 1 clauses back subsumed 0 clauses not processed 1 fpa argument overloads 2 ----------- times (seconds) ----------- run time 0.16 (run time 0 hr, 0 min, 0 sec) input time 0.10 clausify time 0.00 hyper_res time 0.00 pre_process time 0.00 demod time 0.00 lex_rpo time 0.00 for_sub time 0.00 unit_del time 0.00 renumber time 0.00 cl integrate 0.00 print_cl time 0.00 post_process time 0.01 conflict time 0.00 back_sub time 0.00 FPA build time 0.00 IS build time 0.01 weigh cl time 0.00 window time 0.00