% problem-set/geometry/tarski/t4.ver1.out % created : 08/17/89 % revised : 08/17/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Aug 17 18:40:38 1989 set(hyper_res). set(ur_res). set(factor). set(dynamic_demod). set(order_eq). set(unit_deletion). assign(stats_level,1). assign(max_mem,2000). assign(max_seconds,1800). set_skolem([ext(x,y,z,w),op(u,v,w,x,y)]). set_skolem([euc1(u,v,w,x,y),euc2(u,v,w,x,y),cont(u,v,w,x,y,z)]). set(delete_identical_nested_skolem). assign(max_weight,50). list(axioms). 1 [] EQUAL(x,x). 2 [] -EQUAL(x,y) | EQUAL(y,x). 3 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 4 [] -B(x,w,z) | B(y,w,z) | -EQUAL(x,y). 5 [] -B(w,x,z) | B(w,y,z) | -EQUAL(x,y). 6 [] -B(w,z,x) | B(w,z,y) | -EQUAL(x,y). 7 [] -C(x,w,z) | C(y,w,z) | -EQUAL(x,y). 8 [] -C(w,x,z) | C(w,y,z) | -EQUAL(x,y). 9 [] -C(w,z,x) | C(w,z,y) | -EQUAL(x,y). 10 [] -L(x,v,w,z) | L(y,v,w,z) | -EQUAL(x,y). 11 [] -L(v,x,w,z) | L(v,y,w,z) | -EQUAL(x,y). 12 [] -L(v,w,x,z) | L(v,w,y,z) | -EQUAL(x,y). 13 [] -L(v,w,z,x) | L(v,w,y,z) | -EQUAL(x,y). 14 [] EQUAL(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)) | -EQUAL(x,y). 15 [] EQUAL(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)) | -EQUAL(x,y). 16 [] EQUAL(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)) | -EQUAL(x,y). 17 [] EQUAL(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)) | -EQUAL(x,y). 18 [] EQUAL(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)) | -EQUAL(x,y). 19 [] EQUAL(euc1(x,v1,v2,v3,v4),euc1(y,v1,v2,v3,v4)) | -EQUAL(x,y). 20 [] EQUAL(euc1(v1,x,v2,v3,v4),euc1(v1,y,v2,v3,v4)) | -EQUAL(x,y). 21 [] EQUAL(euc1(v1,v2,x,v3,v4),euc1(v1,v2,y,v3,v4)) | -EQUAL(x,y). 22 [] EQUAL(euc1(v1,v2,v3,x,v4),euc1(v1,v2,v3,y,v4)) | -EQUAL(x,y). 23 [] EQUAL(euc1(v1,v2,v3,v4,x),euc1(v1,v2,v3,v4,y)) | -EQUAL(x,y). 24 [] EQUAL(euc2(x,v1,v2,v3,v4),euc2(y,v1,v2,v3,v4)) | -EQUAL(x,y). 25 [] EQUAL(euc2(v1,x,v2,v3,v4),euc2(v1,y,v2,v3,v4)) | -EQUAL(x,y). 26 [] EQUAL(euc2(v1,v2,x,v3,v4),euc2(v1,v2,y,v3,v4)) | -EQUAL(x,y). 27 [] EQUAL(euc2(v1,v2,v3,x,v4),euc2(v1,v2,v3,y,v4)) | -EQUAL(x,y). 28 [] EQUAL(euc2(v1,v2,v3,v4,x),euc2(v1,v2,v3,v4,y)) | -EQUAL(x,y). 29 [] EQUAL(ext(x,v1,v2,v3),ext(y,v1,v2,v3)) | -EQUAL(x,y). 30 [] EQUAL(ext(v1,x,v2,v3),ext(v1,y,v2,v3)) | -EQUAL(x,y). 31 [] EQUAL(ext(v1,v2,x,v3),ext(v1,v2,y,v3)) | -EQUAL(x,y). 32 [] EQUAL(ext(v1,v2,v3,x),ext(v1,v2,v3,y)) | -EQUAL(x,y). 33 [] EQUAL(cont(x,v1,v2,v3,v4,v5),cont(y,v1,v2,v3,v4,v5)) | -EQUAL(x,y). 34 [] EQUAL(cont(v1,x,v2,v3,v4,v5),cont(v1,y,v2,v3,v4,v5)) | -EQUAL(x,y). 35 [] EQUAL(cont(v1,v2,x,v3,v4,v5),cont(v1,v2,y,v3,v4,v5)) | -EQUAL(x,y). 36 [] EQUAL(cont(v1,v2,v3,x,v4,v5),cont(v1,v2,v3,y,v4,v5)) | -EQUAL(x,y). 37 [] EQUAL(cont(v1,v2,v3,v4,x,v5),cont(v1,v2,v3,v4,y,v5)) | -EQUAL(x,y). 38 [] EQUAL(cont(v1,v2,v3,v4,v5,x),cont(v1,v2,v3,v4,v5,y)) | -EQUAL(x,y). end_of_list. list(sos). 39 [] -B(x,y,x) | EQUAL(x,y). 40 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 41 [] -B(x,y,z) | -B(x,y,v) | B(x,z,v) | B(x,v,z) | EQUAL(x,y). 42 [] L(x,y,y,x). 43 [] -L(x,y,z,z) | EQUAL(x,y). 44 [] -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). 45 [] B(x,op(w,x,y,z,v),y) | -B(x,w,v) | -B(y,v,z). 46 [] B(z,w,op(w,x,y,z,v)) | -B(x,w,v) | -B(y,v,z). 47 [] B(u,v,euc1(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) | EQ(u,w). 48 [] B(u,x,euc2(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) | EQ(u,w). 49 [] B(euc1(u,v,w,x,y),y,euc2(u,v,w,x,y)) | -B(u,w,y) | -B(v,w,x) | EQ(u,w). 50 [] -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) | EQUAL(x,y). 51 [] B(x,y,ext(x,y,w,v)). 52 [] L(y,ext(x,y,w,v),w,v). 53 [] -B(C1,C2,C3). 54 [] -B(C2,C3,C1). 55 [] -B(C3,C1,C2). 56 [] -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) | EQUAL(w,v). 57 [] -L(v,y,v,cont(x,y,z,x1,z1,v)) | L(v,x,v,x1) | -L(v,z,v,z1) | -B(v,x,z) | -B(x,y,z). 58 [] -L(v,x,v,x1) | -L(v,z,v,z1) | B(x1,cont(x,y,z,x1,z1,v),z1) | -B(v,x,z) | -B(x,y,z). 59 [] -C(x,y,z) | B(x,y,z) | B(y,x,z) | B(x,z,y). 60 [] -B(x,y,z) | C(x,y,z). 61 [] -B(y,x,z) | C(x,y,z). 62 [] -B(x,z,y) | C(x,y,z). 63 [] -EQUAL(a,b). 64 [] -L(a,x,b,x) | -B(a,x,b) | $ANS(x). 65 [] -B(x,y,z) | B(z,y,x). 66 [] B(x,x,y). 67 [] B(x,y,y). 68 [] -B(x,y,z) | -B(x,z,y) | EQUAL(x,y) | EQUAL(y,z) | EQUAL(x,z). 69 [] -B(x,y,z) | -B(y,x,z) | EQUAL(x,y) | EQUAL(y,z) | EQUAL(x,z). 70 [] -B(w,y,z) | -B(x,y,z) | B(x,w,y) | B(w,x,y) | EQUAL(y,z). 71 [] -B(x,y,z) | -B(x,w,z) | -B(y,v,w) | B(x,v,z). 72 [] -C(x,y,z) | C(x,z,y). 73 [] -C(x,y,z) | C(y,x,z). 74 [] -C(x,y,z) | C(y,z,x). 75 [] -C(x,y,z) | C(z,x,y). 76 [] -C(x,y,z) | C(z,y,x). 77 [] -C(C1,C2,C3). end_of_list. list(demodulators). 78 [] EQUAL(ext(x,y,z,z),y). end_of_list. weight_list(pick_and_purge). weight(x,10). weight(C1,1). weight(C2,1). weight(C3,1). weight(a,0). weight(b,0). weight(ext(2,2,2,2),10). weight(op(2,2,2,2,2),10). weight(euc1(2,2,2,2,2),10). weight(euc2(2,2,2,2,2),10). weight(cont(2,2,2,2,2,2),10). end_of_list. ------------ END OF SEARCH ------------ sos empty. ------------- memory usage ------------ 6 mallocs of 32700 bytes each (191.6+ K) type (bytes each) gets frees in use avail bytes -------------- statistics ------------- clauses generated 6316 clauses kept 257 clauses forward subsumed 3745 clauses back subsumed 35 ----------- times (seconds) ----------- run time 269.55 hyper_res time 2.36 UR_res time 208.07 for_sub time 16.18 back_sub time 0.62 conflict time 0.89 demod time 9.75