% problem-set/algebra/category.theory/p7.ver3.out % created : 07/07/89 % revised : 07/07/89 --------- OTTER 1.03+, 1989 --------- Job run on Fri Jul 7 11:09:20 1989 set(para_into). set(para_from_left). 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 [] -E(dom(x)) | E(x). 3 [] -E(dom(x)) | (dom(x) != cod(y)) | E(star(x,y)). end_of_list. -------> sos clausifies to: list(sos). 4 [] E(dom(c1)). 5 [] E(dom(c2)). 6 [] (dom(c1) = cod(c2)). 7 [] -E(star(c1,c2)). end_of_list. ----> UNIT CONFLICT at 0.35 sec ----> 14 [binary,12,4] . ---------------- PROOF ---------------- 3 [] -E(dom(x)) | (dom(x) != cod(y)) | E(star(x,y)). 4 [] E(dom(c1)). 6 [] (dom(c1) = cod(c2)). 7 [] -E(star(c1,c2)). 12 [ur,6,3,7] -E(dom(c1)). 14 [binary,12,4] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 0 clauses given 6 clauses generated 6 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 0 (subsumed by sos) 0 clauses kept 7 new demodulators 0 empty clauses 1 clauses back subsumed 0 clauses not processed 3 ----------- times (seconds) ----------- run time 0.50 (run time 0 hr, 0 min, 0 sec) input time 0.21 clausify time 0.03 UR_res time 0.03 para_into time 0.00 pre_process time 0.05 demod time 0.00 for_sub time 0.01 renumber time 0.00 cl integrate 0.01 print_cl time 0.02 post_process time 0.04 conflict time 0.01 back_sub time 0.00 FPA build time 0.02 IS build time 0.01 weigh cl time 0.00 window time 0.00