% problem-set/algebra/category.theory/p14.ver2.out % created : 07/07/89 % revised : 07/07/89 --------- OTTER 1.03+, 1989 --------- Job run on Fri Jul 7 16:34:16 1989 set(ur_res). set(para_into). set(para_from_left). set(para_from_right). set(dynamic_demod). 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)). end_of_list. list(sos). 9 [] (cod(cod(a)) != cod(a)). end_of_list. list(demodulators). 10 [] (cod(dom(x)) = dom(x)). 11 [] (dom(cod(x)) = cod(x)). 12 [] (star(dom(x),x) = x). 13 [] (star(x,cod(x)) = x). end_of_list. ----> UNIT CONFLICT at 0.72 sec ----> 26 [binary,25,1] . ---------------- PROOF ---------------- 1 [] (x = x). 7 [] (cod(x) != dom(y)) | (cod(star(x,y)) = cod(y)). 9 [] (cod(cod(a)) != cod(a)). 11 [] (dom(cod(x)) = cod(x)). 13 [] (star(x,cod(x)) = x). 15 [para_into,9,7,demod,11] (cod(star(x,cod(a))) != cod(a)) | (cod(x) != cod(a)). 25 [ur,15,1,demod,13] (cod(a) != cod(a)). 26 [binary,25,1] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 5 clauses given 3 clauses generated 23 demod & eval rewrites 13 tautologies deleted 0 clauses forward subsumed 11 (subsumed by sos) 0 clauses kept 13 new demodulators 0 empty clauses 1 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 0.85 (run time 0 hr, 0 min, 0 sec) input time 0.30 clausify time 0.03 UR_res time 0.01 para_into time 0.04 pre_process time 0.30 demod time 0.04 for_sub time 0.08 renumber time 0.01 cl integrate 0.02 print_cl time 0.07 post_process time 0.06 conflict time 0.00 back_sub time 0.02 FPA build time 0.05 IS build time 0.02 weigh cl time 0.01 window time 0.00