% problem-set/algebra/category.theory/p8.ver1.out % created : 07/03/89 % revised : 07/03/89 --------- OTTER 1.03+, 1989 --------- Job run on Mon Jul 3 14:48:04 1989 set(hyper_res). set(ur_res). set(dynamic_demod). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). list(axioms). 1 [] -DEF(x,y) | P(x,y,star(x,y)). 2 [] -P(x,y,z) | DEF(x,y). 3 [] -P(x,y,xy) | -DEF(xy,z) | DEF(y,z). 4 [] -P(x,y,xy) | -P(y,z,yz) | -DEF(xy,z) | DEF(x,yz). 5 [] -P(x,y,xy) | -P(xy,z,xyz) | -P(y,z,yz) | P(x,yz,xyz). 6 [] -P(y,z,yz) | -DEF(x,yz) | DEF(x,y). 7 [] -P(y,z,yz) | -P(x,y,xy) | -DEF(x,yz) | DEF(xy,z). 8 [] -P(y,z,yz) | -P(x,yz,xyz) | -P(x,y,xy) | P(xy,z,xyz). 9 [] -DEF(x,y) | -DEF(y,z) | -IDENT(y) | DEF(x,z). 10 [] IDENT(dom(x)). 11 [] IDENT(cod(x)). 12 [] DEF(x,dom(x)). 13 [] DEF(cod(x),x). 14 [] P(x,dom(x),x). 15 [] P(cod(x),x,x). 16 [] -DEF(x,y) | -IDENT(x) | P(x,y,y). 17 [] -DEF(x,y) | -IDENT(y) | P(x,y,x). 18 [] EQUAL(x,x). 19 [] -EQUAL(x,y) | EQUAL(y,x). 20 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 21 [] -EQUAL(x,y) | -P(x,z,w) | P(y,z,w). 22 [] -EQUAL(x,y) | -P(z,x,w) | P(z,y,w). 23 [] -EQUAL(x,y) | -P(z,w,x) | P(z,w,y). 24 [] -EQUAL(x,y) | EQUAL(dom(x),dom(y)). 25 [] -EQUAL(x,y) | EQUAL(cod(x),cod(y)). 26 [] -EQUAL(x,y) | -IDENT(x) | IDENT(y). 27 [] -EQUAL(x,y) | -DEF(x,z) | DEF(y,z). 28 [] -EQUAL(x,y) | -DEF(z,x) | DEF(z,y). 29 [] -EQUAL(x,y) | EQUAL(star(z,x),star(z,y)). 30 [] -EQUAL(x,y) | EQUAL(star(x,z),star(y,z)). 31 [] -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). end_of_list. list(sos). 32 [] DEF(a,b). 33 [] -EQUAL(dom(a),cod(b)). end_of_list. ----> UNIT CONFLICT at 23.96 sec ----> 341 [binary,340,65] . ---------------- PROOF ---------------- 3 [] -P(x,y,xy) | -DEF(xy,z) | DEF(y,z). 6 [] -P(y,z,yz) | -DEF(x,yz) | DEF(x,y). 10 [] IDENT(dom(x)). 11 [] IDENT(cod(x)). 14 [] P(x,dom(x),x). 15 [] P(cod(x),x,x). 16 [] -DEF(x,y) | -IDENT(x) | P(x,y,y). 17 [] -DEF(x,y) | -IDENT(y) | P(x,y,x). 18 [] EQUAL(x,x). 20 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 31 [] -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). 32 [] DEF(a,b). 33 [] -EQUAL(dom(a),cod(b)). 34 [hyper,32,6,15] DEF(a,cod(b)). 40 [hyper,34,3,14] DEF(dom(a),cod(b)). 50 [ur,33,20,18] -EQUAL(cod(b),dom(a)). 64 [hyper,40,17,11] P(dom(a),cod(b),dom(a)). 65 [hyper,40,16,10] P(dom(a),cod(b),cod(b)). 340 [ur,64,31,50] -P(dom(a),cod(b),cod(b)). 341 [binary,340,65] . ------------ end of proof ------------- ------------- memory usage ------------ 4 mallocs of 32700 bytes each (127.7+ K) -------------- statistics ------------- clauses input 33 clauses given 61 clauses generated 2016 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 1709 (subsumed by sos) 598 clauses kept 308 new demodulators 0 empty clauses 1 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 24.11 (run time 0 hr, 0 min, 24 sec) input time 0.48 clausify time 0.00 hyper_res time 4.17 UR_res time 9.22 pre_process time 7.87 demod time 0.00 for_sub time 4.24 renumber time 0.65 cl integrate 0.27 print_cl time 1.09 post_process time 1.66 conflict time 1.03 back_sub time 0.39 FPA build time 0.41 IS build time 0.17 weigh cl time 0.09 window time 0.00