% problem-set/geometry/tarski/t1.ver1.out % created : 07/20/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Jul 20 08:46:11 1989 set(hyper_res). set(ur_res). set(dynamic_demod). set(order_eq). assign(max_seconds,1800). 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)). end_of_list. list(sos). 34 [] B(a,b,c). 35 [] -B(c,b,a). end_of_list. weight_list(purge_gen). weight(x,20). end_of_list. ----> UNIT CONFLICT at 30.79 sec ----> 294 [binary,291,280] . ---------------- 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)). 19 [] -EQUAL(x,y) | -B(w,x,z) | B(w,y,z). 20 [] -EQUAL(x,y) | -B(w,z,x) | B(w,z,y). 34 [] B(a,b,c). 35 [] -B(c,b,a). 36 [hyper,34,3,34] EQUAL(b,a) | B(a,c,c). 39 [hyper,36,8,34] EQUAL(b,a) | B(c,b,op(b,a,a,c,c)). 40 [hyper,36,7,36] EQUAL(b,a) | B(a,op(c,a,a,c,c),a). 41 [hyper,36,7,34] EQUAL(b,a) | B(a,op(b,a,a,c,c),a). 152 [hyper,40,1] EQUAL(b,a) | EQUAL(op(c,a,a,c,c),a). 155 [hyper,152,19,40] EQUAL(b,a) | B(a,a,a). 171 [hyper,155,19,34] B(a,a,a) | B(a,a,c). 211 [hyper,171,2,171] B(a,a,a). 214 [hyper,211,7,211] B(a,op(a,a,a,a,a),a). 255 [hyper,214,1] EQUAL(op(a,a,a,a,a),a). 256 [new_demod,255] EQUAL(op(a,a,a,a,a),a). 262 [hyper,41,1] EQUAL(b,a) | EQUAL(op(b,a,a,c,c),a). 264 [hyper,262,20,39] EQUAL(b,a) | B(c,b,a). 266 [hyper,264,35] EQUAL(b,a). 267 [new_demod,266] EQUAL(b,a). 268 [hyper,266,19,34] B(a,a,c). 269 [ur,266,20,35,demod,267,267] -B(c,a,a). 270 [hyper,268,8,214,demod,256,256] B(c,a,op(a,a,a,c,a)). 271 [hyper,268,7,214,demod,256] B(a,op(a,a,a,c,a),a). 280 [ur,270,2,269] -B(a,a,op(a,a,a,c,a)). 291 [hyper,271,2,211] B(a,a,op(a,a,a,c,a)). 294 [binary,291,280] . ------------ end of proof ------------- ------------- memory usage ------------ 5 mallocs of 32700 bytes each (159.7+ K) -------------- statistics ------------- clauses input 35 clauses given 35 clauses generated 1987 demod & eval rewrites 302 clauses wt or lit delete 531 tautologies deleted 0 clauses forward subsumed 1201 (subsumed by sos) 271 clauses kept 256 new demodulators 3 empty clauses 1 clauses back subsumed 168 clauses not processed 11 fpa argument overloads 252 fpa argument underloads 130 ----------- times (seconds) ----------- run time 31.01 (run time 0 hr, 0 min, 31 sec) input time 0.71 clausify time 0.00 hyper_res time 6.00 UR_res time 4.46 pre_process time 15.17 demod time 0.70 lex_rpo time 0.00 for_sub time 7.55 renumber time 1.05 cl integrate 0.33 print_cl time 1.14 post_process time 4.07 conflict time 0.16 back_sub time 2.11 FPA build time 0.55 IS build time 0.22 weigh cl time 1.49 window time 0.00