% problem-set/algebra/category.theory/p6.ver3.out % created : 07/07/89 % revised : 07/07/89 --------- OTTER 1.03+, 1989 --------- Job run on Fri Jul 7 11:21:34 1989 set(hyper_res). set(ur_res). set(dynamic_demod). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). -------> axioms clausifies to: list(axioms). 1 [] (x = x). 2 [] -ee(x,y) | E(x). 3 [] -ee(x,y) | (x = y). 4 [] -E(x) | (x != y) | ee(x,y). 5 [] -E(dom(x)) | E(x). 6 [] -E(cod(x)) | E(x). 7 [] -E(star(x,y)) | E(dom(x)). 8 [] -E(star(x,y)) | (dom(x) = cod(y)). 9 [] -E(dom(x)) | (dom(x) != cod(y)) | E(star(x,y)). 10 [] (star(x,star(y,z)) = star(star(x,y),z)). 11 [] (star(x,dom(x)) = x). 12 [] (star(cod(x),x) = x). 13 [] (x != y) | -E(x) | E(y). 14 [] (x != y) | -ee(x,z) | ee(y,z). 15 [] (x != y) | -ee(z,x) | ee(z,y). 16 [] (x != y) | (x != z) | (y = z). 17 [] (x != y) | (z != x) | (z = y). 18 [] (x != y) | (dom(x) = dom(y)). 19 [] (x != y) | (cod(x) = cod(y)). 20 [] (x != y) | (star(x,z) = star(y,z)). 21 [] (x != y) | (star(z,x) = star(z,y)). 22 [] -ee(x,y) | E(y). 23 [] -E(x) | -E(y) | (x != y) | ee(x,y). 24 [] -E(star(x,y)) | E(cod(x)). 25 [] (x != z) | (y != z) | (x = y). 26 [] (x = z) | (y = z) | (x = y). end_of_list. list(sos). 27 [] E(star(d,a)). 28 [] -E(star(x,d)) | (star(x,d) = x). 29 [] -E(star(d,x)) | (star(d,x) = x). 30 [] (cod(a) != d). end_of_list. ----> UNIT CONFLICT at 146.46 sec ----> 691 [binary,689,272] . ---------------- PROOF ---------------- 6 [] -E(cod(x)) | E(x). 7 [] -E(star(x,y)) | E(dom(x)). 8 [] -E(star(x,y)) | (dom(x) = cod(y)). 12 [] (star(cod(x),x) = x). 13 [] (x != y) | -E(x) | E(y). 16 [] (x != y) | (x != z) | (y = z). 17 [] (x != y) | (z != x) | (z = y). 24 [] -E(star(x,y)) | E(cod(x)). 25 [] (x != z) | (y != z) | (x = y). 26 [] (x = z) | (y = z) | (x = y). 27 [] E(star(d,a)). 28 [] -E(star(x,d)) | (star(x,d) = x). 30 [] (cod(a) != d). 31 [hyper,27,24] E(cod(d)). 36 [hyper,27,8] (cod(a) = dom(d)). 37 [hyper,27,7] E(dom(d)). 45 [hyper,31,6] E(d). 76 [hyper,30,26] (cod(a) = x) | (d = x). 97 [ur,36,25,30] (dom(d) != d). 144 [hyper,76,13,45] (cod(a) = x) | E(x). 162 [hyper,144,16,36] E(x) | (dom(d) = x). 228 [hyper,162,13,37] E(x). 237 [hyper,228,8] (cod(y) = dom(x)). 261 [ur,237,16,97] (cod(x) != d). 272 [ur,261,17,12] (star(cod(d),d) != cod(x)). 689 [hyper,28,228] (star(x,d) = x). 691 [binary,689,272] . ------------ end of proof ------------- ------------- memory usage ------------ 10 mallocs of 32700 bytes each (319.3+ K) -------------- statistics ------------- clauses input 4 clauses given 82 clauses generated 4311 demod & eval rewrites 3476 tautologies deleted 0 clauses forward subsumed 3656 (subsumed by sos) 1764 clauses kept 656 new demodulators 5 empty clauses 1 clauses back subsumed 282 clauses not processed 2 ----------- times (seconds) ----------- run time 146.62 (run time 0 hr, 2 min, 26 sec) input time 0.91 clausify time 0.13 hyper_res time 7.90 UR_res time 3.61 pre_process time 120.37 demod time 4.68 for_sub time 100.22 renumber time 2.38 cl integrate 0.87 print_cl time 3.70 post_process time 12.08 conflict time 1.46 back_sub time 7.08 FPA build time 1.39 IS build time 0.62 weigh cl time 0.29 window time 0.00