% problem-set/algebra/category.theory/p3.ver2.out % created : 07/07/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Mon Jul 10 15:04:44 1989 set(ur_res). set(sos_queue). set(para_into). set(para_from_left). set(para_from_right). set(dynamic_demod_all). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). -------> axioms clausifies to: list(axioms). 1 [] (x = x). 2 [] (cod(dom(x)) = dom(x)). 3 [] (dom(cod(x)) = cod(x)). 4 [] (star(dom(x),x) = x). 5 [] (star(x,cod(x)) = x). 6 [] (cod(x) != dom(y)) | (dom(star(x,y)) = dom(x)). 7 [] (cod(x) != dom(y)) | (cod(star(x,y)) = cod(y)). 8 [] (cod(x) != dom(y)) | (cod(y) != dom(z)) | (star(x,star(y,z)) = star(star(x,y),z)). 9 [] (cod(star(a,b)) != dom(x)) | (star(star(a,b),x) != y) | (cod(star(a,b)) != dom(z)) | (star(star(a,b),z) != y) | (x = z). end_of_list. list(sos). 10 [] (cod(a) = dom(b)). 11 [] (cod(b) = dom(h)). 12 [] (cod(b) = dom(g)). 13 [] (star(b,h) = star(b,g)). 14 [] (g != h). end_of_list. list(demodulators). 15 [] (cod(dom(x)) = dom(x)). 16 [] (dom(cod(x)) = cod(x)). 17 [] (star(dom(x),x) = x). 18 [] (star(x,cod(x)) = x). end_of_list. OTTER sets dynamic_demod, because dynamic_demod_all is set. ------------ END OF SEARCH ------------ search stopped by max_seconds option. no proof in 86 given clauses, 4049 kept clauses, 30 minutes runtime. ------------- memory usage ------------ 93 mallocs of 32700 bytes each (2969.8+ K) -------------- statistics ------------- clauses input 9 clauses given 86 clauses generated 7164 demod & eval rewrites 3288 tautologies deleted 0 clauses forward subsumed 3115 (subsumed by sos) 1059 clauses kept 4049 new demodulators 18 empty clauses 0 clauses back subsumed 268 clauses not processed 0 ----------- times (seconds) ----------- run time 1836.19 (run time 0 hr, 30 min, 36 sec) input time 0.40 clausify time 0.04 UR_res time 0.78 para_into time 17.36 pre_process time 1508.61 demod time 22.26 for_sub time 1396.80 renumber time 5.37 cl integrate 10.87 print_cl time 35.67 post_process time 305.69 conflict time 0.47 back_sub time 287.56 FPA build time 12.86 IS build time 6.67 weigh cl time 3.73 window time 0.00