% problem-set/algebra/category.theory/p15.ver3.no2.out % created : 07/10/89 % revised : 07/12/89 --------- OTTER 1.03+, 1989 --------- Job run on Mon Jul 10 16:49:56 1989 set(ur_res). set(dynamic_demod_all). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). -------> axioms clausifies to: list(axioms). 1 [] (x = x). 2 [] (x = y) | E(x) | E(y). 3 [] -ee(x,y) | E(x). 4 [] -ee(x,y) | (x = y). 5 [] -E(x) | (x != y) | ee(x,y). 6 [] (x != y) | -E(x) | E(y). 7 [] (x != y) | -ee(x,z) | ee(y,z). 8 [] (x != y) | -ee(z,x) | ee(z,y). 9 [] (x != y) | (x != z) | (y = z). 10 [] (x != y) | (z != x) | (z = y). 11 [] -ee(x,y) | E(y). 12 [] -E(x) | -E(y) | (x != y) | ee(x,y). end_of_list. -------> sos clausifies to: list(sos). 13 [] -E(z) | (a != z) | (b = z). 14 [] -E(z) | (a = z) | (b != z). 15 [] (a != b). end_of_list. OTTER sets dynamic_demod, because dynamic_demod_all is set. ----> UNIT CONFLICT at 0.73 sec ----> 28 [binary,24,22] . ---------------- PROOF ---------------- 1 [] (x = x). 2 [] (x = y) | E(x) | E(y). 10 [] (x != y) | (z != x) | (z = y). 13 [] -E(z) | (a != z) | (b = z). 14 [] -E(z) | (a = z) | (b != z). 15 [] (a != b). 16 [ur,15,10,1] (b != a). 19 [ur,13,1,16] -E(a). 22 [ur,19,2,16] E(b). 24 [ur,14,15,1] -E(b). 28 [binary,24,22] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 0 clauses given 11 clauses generated 44 demod & eval rewrites 2 tautologies deleted 0 clauses forward subsumed 33 (subsumed by sos) 6 clauses kept 12 new demodulators 1 empty clauses 1 clauses back subsumed 2 clauses not processed 0 ----------- times (seconds) ----------- run time 0.84 (run time 0 hr, 0 min, 0 sec) input time 0.37 clausify time 0.05 UR_res time 0.13 pre_process time 0.15 demod time 0.01 for_sub time 0.06 renumber time 0.01 cl integrate 0.00 print_cl time 0.02 post_process time 0.05 conflict time 0.01 back_sub time 0.00 FPA build time 0.03 IS build time 0.01 weigh cl time 0.00 window time 0.00