--------- OTTER 1.03+, 1989 --------- Job run on Tue Aug 8 14:52:40 1989 set(dynamic_demod). set(para_from). set(para_into). set(para_from_right). set(para_from_left). assign(max_seconds,40). list(axioms). 1 [] (x = x). 2 [] (sum(x,y) = sum(y,x)). 3 [] (prod(x,y) = prod(y,x)). 4 [] (sum(prod(x,y),z) = prod(sum(x,z),sum(y,z))). 5 [] (sum(x,prod(y,z)) = prod(sum(x,y),sum(x,z))). 6 [] (prod(sum(x,y),z) = sum(prod(x,z),prod(y,z))). 7 [] (prod(x,sum(y,z)) = sum(prod(x,y),prod(x,z))). end_of_list. list(sos). 8 [] (sum(x,comp(x)) = 1). 9 [] (sum(comp(x),x) = 1). 10 [] (prod(x,comp(x)) = 0). 11 [] (prod(comp(x),x) = 0). 12 [] (sum(x,0) = x). 13 [] (sum(0,x) = x). 14 [] (prod(x,1) = x). 15 [] (prod(1,x) = x). 16 [] (prod(a,0) != 0). end_of_list. list(demodulators). lex-dependent demodulator: (sum(x,y) = sum(y,x)) lex-dependent demodulator: (prod(x,y) = prod(y,x)) 17 [] (sum(x,y) = sum(y,x)). 18 [] (prod(x,y) = prod(y,x)). 19 [] (sum(prod(x,y),z) = prod(sum(x,z),sum(y,z))). 20 [] (sum(z,prod(x,y)) = prod(sum(z,x),sum(z,y))). 21 [] (sum(x,comp(x)) = 1). 22 [] (sum(comp(x),x) = 1). 23 [] (prod(x,comp(x)) = 0). 24 [] (prod(comp(x),x) = 0). 25 [] (sum(x,0) = x). 26 [] (sum(0,x) = x). 27 [] (prod(x,1) = x). 28 [] (prod(1,x) = x). end_of_list. OTTER sets order_eq, because dynamic_demod is set. ----> UNIT CONFLICT at 6.21 sec ----> 104 [binary,89,16] . ---------------- PROOF ---------------- 7 [] (prod(x,sum(y,z)) = sum(prod(x,y),prod(x,z))). 10 [] (prod(x,comp(x)) = 0). 13 [] (sum(0,x) = x). 16 [] (prod(a,0) != 0). 23 [] (prod(x,comp(x)) = 0). 25 [] (sum(x,0) = x). 66 [para_from,10,7,demod,25] (prod(x,sum(y,comp(x))) = prod(x,y)). 89 [para_into,66,13,demod,23] (prod(x,0) = 0). 104 [binary,89,16] . ------------ end of proof ------------- ------------- memory usage ------------ 3 mallocs of 32700 bytes each (95.8+ K) type (bytes each) gets frees in use avail bytes -------------- statistics ------------- clauses input 28 clauses given 13 clauses generated 222 demod & eval rewrites 352 tautologies deleted 0 clauses forward subsumed 173 (subsumed by sos) 6 clauses kept 50 new demodulators 26 empty clauses 1 clauses back subsumed 0 clauses not processed 15 ----------- times (seconds) ----------- run time 6.41 (run time 0 hr, 0 min, 6 sec) input time 0.86 clausify time 0.00 para_into time 0.24 para_from time 0.33 pre_process time 4.43 demod time 1.78 for_sub time 0.56 renumber time 0.31 cl integrate 0.18 print_cl time 0.52 post_process time 0.22 conflict time 0.02 back_sub time 0.13 FPA build time 0.30 IS build time 0.07 weigh cl time 0.02 window time 0.00