% problem-set/geometry/tarski/t8.ver1.out % created : 07/20/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 20 10:45:48 1989 set(hyper_res). set(ur_res). set(unit_deletion). assign(max_seconds,1800). set_skolem([ext(x,y,z,w),op(u,v,w,x,y),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,30). list(axioms). 1 [] -B(x,y,x) | EQUAL(x,y). 2 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 3 [] -B(x,y,z) | -B(x,y,v) | EQUAL(x,y) | B(x,z,v) | B(x,v,z). 4 [] L(x,y,y,x). 5 [] -L(x,y,z,z) | EQUAL(x,y). 6 [] -L(x,y,z,v) | -L(x,y,v2,w) | L(z,v,v2,w). 7 [] -B(x,w,v) | -B(y,v,z) | B(x,op(w,x,y,z,v),y). 8 [] -B(x,w,v) | -B(y,v,z) | B(z,w,op(w,x,y,z,v)). 9 [] -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). 10 [] B(x,y,ext(x,y,w,v)). 11 [] L(y,ext(x,y,w,v),w,v). 12 [] -B(C1,C2,C3). 13 [] -B(C2,C3,C1). 14 [] -B(C3,C1,C2). 15 [] EQUAL(x,x). 16 [] -EQUAL(x,y) | EQUAL(y,x). 17 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 18 [] -EQUAL(x,y) | -B(x,w,z) | B(y,w,z). 19 [] -EQUAL(x,y) | -B(w,x,z) | B(w,y,z). 20 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 21 [] -EQUAL(x,y) | -L(x,v,w,z) | L(y,v,w,z). 22 [] -EQUAL(x,y) | -L(v,x,w,z) | L(v,y,w,z). 23 [] -EQUAL(x,y) | -L(v,w,x,z) | L(v,w,y,z). 24 [] -EQUAL(x,y) | -L(v,w,z,x) | L(v,w,y,z). 25 [] -EQUAL(x,y) | EQUAL(op(x,v1,v2,v3,v4),op(y,v1,v2,v3,v4)). 26 [] -EQUAL(x,y) | EQUAL(op(v1,x,v2,v3,v4),op(v1,y,v2,v3,v4)). 27 [] -EQUAL(x,y) | EQUAL(op(v1,v2,x,v3,v4),op(v1,v2,y,v3,v4)). 28 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,x,v4),op(v1,v2,v3,y,v4)). 29 [] -EQUAL(x,y) | EQUAL(op(v1,v2,v3,v4,x),op(v1,v2,v3,v4,y)). 30 [] -EQUAL(x,y) | EQUAL(ext(x,v1,v2,v3),ext(y,v1,v2,v3)). 31 [] -EQUAL(x,y) | EQUAL(ext(v1,x,v2,v3),ext(v1,y,v2,v3)). 32 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,x,v3),ext(v1,v2,y,v3)). 33 [] -EQUAL(x,y) | EQUAL(ext(v1,v2,v3,x),ext(v1,v2,v3,y)). 34 [] -B(x,y,z) | B(z,y,x). 35 [] B(x,y,y). end_of_list. list(sos). 36 [] B(a,c,e). 37 [] B(a,d,e). 38 [] B(c,b,d). 39 [] -B(a,b,e). end_of_list. weight_list(purge_gen). weight(x,20). weight(C1,0). weight(C2,0). weight(C3,0). weight(a,0). weight(b,0). weight(c,0). weight(d,0). weight(e,0). end_of_list. ----> UNIT CONFLICT at 260.18 sec ----> 855 [binary,854,778] . ---------------- PROOF ---------------- 1 [] -B(x,y,x) | EQUAL(x,y). 2 [] -B(x,y,v) | -B(y,z,v) | B(x,y,z). 3 [] -B(x,y,z) | -B(x,y,v) | EQUAL(x,y) | B(x,z,v) | B(x,v,z). 7 [] -B(x,w,v) | -B(y,v,z) | B(x,op(w,x,y,z,v),y). 8 [] -B(x,w,v) | -B(y,v,z) | B(z,w,op(w,x,y,z,v)). 16 [] -EQUAL(x,y) | EQUAL(y,x). 18 [] -EQUAL(x,y) | -B(x,w,z) | B(y,w,z). 20 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 34 [] -B(x,y,z) | B(z,y,x). 36 [] B(a,c,e). 37 [] B(a,d,e). 38 [] B(c,b,d). 39 [] -B(a,b,e). 40 [hyper,36,34] B(e,c,a). 43 [hyper,37,34] B(e,d,a). 48 [hyper,38,8,37] B(e,b,op(b,c,a,e,d)). 50 [hyper,38,7,37] B(c,op(b,c,a,e,d),a). 51 [ur,39,34] -B(e,b,a). 66 [hyper,43,8,38] B(a,b,op(b,c,e,a,d)). 69 [hyper,43,7,38] B(c,op(b,c,e,a,d),e). 98 [hyper,48,34] B(op(b,c,a,e,d),b,e). 100 [ur,48,20,51] -EQUAL(op(b,c,a,e,d),a). 102 [ur,48,2,51] -B(b,a,op(b,c,a,e,d)). 105 [ur,100,16] -EQUAL(a,op(b,c,a,e,d)). 108 [ur,105,1] -B(a,op(b,c,a,e,d),a). 115 [hyper,50,34] B(a,op(b,c,a,e,d),c). 116 [hyper,50,2,40] B(e,c,op(b,c,a,e,d)). 121 [ur,66,20,39] -EQUAL(op(b,c,e,a,d),e). 123 [ur,66,2,39] -B(b,e,op(b,c,e,a,d)). 126 [ur,121,16] -EQUAL(e,op(b,c,e,a,d)). 129 [ur,126,1] -B(e,op(b,c,e,a,d),e). 132 [hyper,69,34] B(e,op(b,c,e,a,d),c). 182 [ur,108,18,50] -EQUAL(c,a). 183 [ur,182,16] -EQUAL(a,c). 204 [ur,115,2,102] -B(b,a,c). 205 [ur,115,2,108] -B(op(b,c,a,e,d),a,c). 209 [ur,204,2,36] -B(b,a,e). 212 [ur,209,34] -B(e,a,b). 221 [ur,129,18,69] -EQUAL(c,e). 222 [ur,221,16] -EQUAL(e,c). 224 [ur,222,3,40,51,212] -B(e,c,b). 240 [ur,224,2,40] -B(c,b,a). 256 [ur,240,34] -B(a,b,c). 326 [ur,132,2,123] -B(b,e,c). 331 [ur,326,2,40] -B(b,e,a). 333 [ur,331,34] -B(a,e,b). 335 [ur,333,3,36,183,39] -B(a,c,b). 348 [ur,335,3,115,105,256] -B(a,op(b,c,a,e,d),b). 528 [ur,205,2,36] -B(op(b,c,a,e,d),a,e). 606 [ur,348,2,98] -B(a,op(b,c,a,e,d),e). 732 [ur,528,34] -B(e,a,op(b,c,a,e,d)). 778 [ur,606,34] -B(e,op(b,c,a,e,d),a). 854 [ur,732,3,116,40,222] B(e,op(b,c,a,e,d),a). 855 [binary,854,778] . ------------ end of proof ------------- ------------- memory usage ------------ 10 mallocs of 32700 bytes each (319.3+ K) -------------- statistics ------------- clauses input 39 clauses given 593 clauses generated 8704 demod & eval rewrites 0 clauses wt or lit delete 2617 tautologies deleted 0 clauses forward subsumed 4840 (subsumed by sos) 428 unit deletions 5 clauses kept 816 empty clauses 1 clauses back subsumed 0 clauses not processed 2 fpa argument overloads 368 ----------- times (seconds) ----------- run time 260.44 (run time 0 hr, 4 min, 20 sec) input time 0.85 clausify time 0.00 hyper_res time 9.93 UR_res time 183.28 pre_process time 52.90 demod time 0.00 lex_rpo time 0.00 for_sub time 21.48 unit_del time 0.04 renumber time 0.31 cl integrate 0.83 print_cl time 2.82 post_process time 8.33 conflict time 4.45 back_sub time 3.16 FPA build time 1.99 IS build time 0.56 weigh cl time 18.82 window time 0.00