% problem-set/geometry/tarski/t9.ver1.out % created : 08/17/89 % revised : 08/17/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Aug 17 18:40:53 1989 lex([a,b,c,d,e,C1,C2,C3,ext(x,y,z,w),op(x,y,z,u,v),B(x,y,z),C(x,y,z),L(x,y,v,w)]). set(hyper_res). set(ur_res). set(dynamic_demod). set(order_eq). set(unit_deletion). assign(max_mem,3000). assign(max_seconds,1800). set_skolem([ext(x,y,z,w),op(u,v,w,x,y)]). set(delete_identical_nested_skolem). assign(max_weight,50). list(axioms). 1 [] EQ(x,x). 2 [] -EQ(x,y) | EQ(y,x). 3 [] -EQ(x,y) | -EQ(y,z) | EQ(x,z). 4 [] -B(x,w,z) | B(y,w,z) | -EQ(x,y). 5 [] -B(w,x,z) | B(w,y,z) | -EQ(x,y). 6 [] -B(w,z,x) | B(w,z,y) | -EQ(x,y). 7 [] -L(x,v,w,z) | L(y,v,w,z) | -EQ(x,y). 8 [] -L(v,x,w,z) | L(v,y,w,z) | -EQ(x,y). 9 [] -L(v,w,x,z) | L(v,w,y,z) | -EQ(x,y). 10 [] -L(v,w,z,x) | L(v,w,y,z) | -EQ(x,y). 11 [] EQ(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)) | -EQ(x,y). 12 [] EQ(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)) | -EQ(x,y). 13 [] EQ(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)) | -EQ(x,y). 14 [] EQ(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)) | -EQ(x,y). 15 [] EQ(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)) | -EQ(x,y). 16 [] EQ(ext(x,v1,v2,v3),ext(y,v1,v2,v3)) | -EQ(x,y). 17 [] EQ(ext(v1,x,v2,v3),ext(v1,y,v2,v3)) | -EQ(x,y). 18 [] EQ(ext(v1,v2,x,v3),ext(v1,v2,y,v3)) | -EQ(x,y). 19 [] EQ(ext(v1,v2,v3,x),ext(v1,v2,v3,y)) | -EQ(x,y). end_of_list. list(sos). 20 [] -B(x,y,x) | EQ(x,y). 21 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 22 [] -B(x,y,z) | -B(x,y,v) | B(x,z,v) | B(x,v,z) | EQ(x,y). 23 [] L(x,y,y,x). 24 [] -L(x,y,z,z) | EQ(x,y). 25 [] -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). 26 [] B(x,op(w,x,y,z,v),y) | -B(x,w,v) | -B(y,v,z). 27 [] B(z,w,op(w,x,y,z,v)) | -B(x,w,v) | -B(y,v,z). 28 [] -L(x,y,x1,y1) | -L(y,z,y1,z1) | -L(x,v,x1,v1) | -L(y,v,y1,v1) | L(z,v,z1,v1) | -B(x,y,z) | -B(x1,y1,z1) | EQ(x,y). 29 [] B(x,y,ext(x,y,w,v)). 30 [] L(y,ext(x,y,w,v),w,v). 31 [] -B(C1,C2,C3). 32 [] -B(C2,C3,C1). 33 [] -B(C3,C1,C2). 34 [] -L(x,w,x,v) | -L(y,w,y,v) | -L(z,w,z,v) | B(x,y,z) | B(y,z,x) | B(z,x,y) | EQ(w,v). 35 [] -B(x,y,z) | B(z,y,x). 36 [] B(x,x,y). 37 [] B(x,y,y). 38 [] -B(x,y,z) | -B(x,z,y) | EQ(x,y) | EQ(y,z) | EQ(x,z). 39 [] -B(x,y,z) | -B(y,x,z) | EQ(x,y) | EQ(y,z) | EQ(x,z). 40 [] -B(w,y,z) | -B(x,y,z) | B(x,w,y) | B(w,x,y) | EQ(y,z). 41 [] -B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z). 42 [] B(a,c,e). 43 [] B(a,d,e). 44 [] -B(a,c,d). 45 [] -B(a,d,c). end_of_list. list(demodulators). lex dependent demodulator: 0 [] (EQ(x,y) = EQ(y,x)). lex dependent demodulator: 0 [] (B(x,y,z) = B(z,y,x)). lex dependent demodulator: 0 [] (L(x,y,z,w) = L(z,w,x,y)). lex dependent demodulator: 0 [] (L(x,y,z,w) = L(x,y,w,z)). lex dependent demodulator: 0 [] (L(x,y,z,w) = L(y,x,z,w)). 46 [] EQ(ext(x,y,z,z),y). 47 [] (B(x,y,x) = EQ(x,y)). 48 [] (L(x,y,z,z) = EQ(x,y)). 49 [] (L(x,y,y,x) = $T). 50 [] (B(C1,C2,C3) = $F). 51 [] (B(C2,C3,C1) = $F). 52 [] (B(C3,C1,C2) = $F). 53 [] (B(x,x,y) = $T). 54 [] (B(x,y,y) = $T). 55 [] (EQ(x,y) = EQ(y,x)). 56 [] (B(x,y,z) = B(z,y,x)). 57 [] (L(x,y,z,w) = L(z,w,x,y)). 58 [] (L(x,y,z,w) = L(x,y,w,z)). 59 [] (L(x,y,z,w) = L(y,x,z,w)). end_of_list. weight_list(pick_and_purge). weight(x,20). weight(C1,1). weight(C2,1). weight(C3,1). weight(a,0). weight(b,0). weight(c,0). weight(d,0). weight(e,0). weight(ext(1,1,1,1),5). weight(op(2,2,2,2,2),5). end_of_list. ------------ END OF SEARCH ------------ sos empty. ------------- memory usage ------------ 4 mallocs of 32700 bytes each (127.7+ K) -------------- statistics ------------- clauses input 59 clauses given 163 clauses generated 3457 demod & eval rewrites 1569 clauses wt,lit,sk delete 848 tautologies deleted 0 clauses forward subsumed 2188 (subsumed by sos) 217 unit deletions 0 clauses kept 137 new demodulators 0 empty clauses 0 clauses back subsumed 0 clauses not processed 0 fpa argument overloads 44 ----------- times (seconds) ----------- run time 74.30 (run time 0 hr, 1 min, 14 sec) input time 1.13 clausify time 0.00 hyper_res time 2.93 UR_res time 33.00 pre_process time 34.66 demod time 11.81 dollar eval 2.17 lex_rpo time 0.00 for_sub time 11.68 unit_del time 0.00 renumber time 1.49 cl integrate 0.11 print_cl time 0.48 post_process time 0.98 conflict time 0.60 back_sub time 0.15 FPA build time 0.39 IS build time 0.10 weigh cl time 5.37 lex_rpo time 0.00 window time 0.00