% problem-set/geometry/tarski/t11.ver2.out % created : 07/25/89 % revised : 07/28/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 27 14:24:19 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). end_of_list. list(sos). 2 [] C(C1,C2,C3). 3 [] D(dist(u,v),dist(v,u)). 4 [] -D(dist(u,v),dist(w,x)) | -D(dist(u,v),dist(y,z)) | D(dist(w,x),dist(y,z)). 5 [] -D(dist(u,v),dist(w,w)) | (u = v). 6 [] B(u,v,ext(u,v,w,x)). 7 [] D(dist(v,ext(u,v,w,x)),dist(w,x)). 8 [] -D(dist(u,v),dist(u1,v1)) | -D(dist(v,w),dist(v1,w1)) | -D(dist(u,x),dist(u1,x1)) | -D(dist(v,x),dist(v1,x1)) | D(dist(w,x),dist(w1,x1)) | -B(u,v,w) | -B(u1,v1,w1) | (u = v). 9 [] -B(u,v,u) | (u = v). 10 [] B(v,ip(u,v,w,x,y),y) | -B(u,v,w) | -B(y,x,w). 11 [] B(x,ip(u,v,w,x,y),u) | -B(u,v,w) | -B(y,x,w). 12 [] -B(C1,C2,C3). 13 [] -B(C2,C3,C1). 14 [] -B(C3,C1,C2). 15 [] -B(u,v,w) | -B(u,v,x) | B(u,w,x) | B(u,x,w) | (u = v). 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). end_of_list. list(demodulators). 20 [] (ext(u,v,u,v) = R(u,v)). 21 [] (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 ----> 22 [hyper,19,2,unit_del,12,13,14] . ---------------- PROOF ---------------- 2 [] C(C1,C2,C3). 12 [] -B(C1,C2,C3). 13 [] -B(C2,C3,C1). 14 [] -B(C3,C1,C2). 19 [] -C(u,v,w) | B(u,v,w) | B(v,w,u) | B(w,u,v). 22 [hyper,19,2,unit_del,12,13,14] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 21 clauses given 13 clauses generated 6 demod & eval rewrites 0 clauses wt or lit delete 5 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.08 clausify time 0.00 hyper_res time 0.01 pre_process time 0.01 demod time 0.00 lex_rpo time 0.00 for_sub time 0.01 unit_del time 0.00 renumber time 0.00 cl integrate 0.00 print_cl time 0.00 post_process time 0.00 conflict time 0.00 back_sub time 0.00 FPA build time 0.01 IS build time 0.00 weigh cl time 0.00 window time 0.00