--------- OTTER 1.03+, 1989 --------- Job run on Wed Aug 9 12:38:04 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 [] (comp(0) != 1). 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 2.19 sec ----> 51 [binary,47,16] . ---------------- PROOF ---------------- 8 [] (sum(x,comp(x)) = 1). 13 [] (sum(0,x) = x). 16 [] (comp(0) != 1). 47 [para_into,8,13] (comp(0) = 1). 51 [binary,47,16] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) type (bytes each) gets frees in use avail bytes -------------- statistics ------------- clauses input 28 clauses given 6 clauses generated 66 demod & eval rewrites 84 tautologies deleted 0 clauses forward subsumed 52 (subsumed by sos) 0 clauses kept 15 new demodulators 8 empty clauses 1 clauses back subsumed 0 clauses not processed 3 ----------- times (seconds) ----------- run time 2.35 (run time 0 hr, 0 min, 2 sec) input time 0.79 clausify time 0.00 para_into time 0.04 para_from time 0.14 pre_process time 1.09 demod time 0.44 for_sub time 0.16 renumber time 0.03 cl integrate 0.03 print_cl time 0.12 post_process time 0.05 conflict time 0.01 back_sub time 0.03 FPA build time 0.12 IS build time 0.01 weigh cl time 0.01 window time 0.00