--------- OTTER 1.03+, 1989 --------- Job run on Tue Aug 8 14:37:21 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 [] (sum(a,1) != 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 11.19 sec ----> 160 [binary,154,47] . ---------------- PROOF ---------------- 2 [] (sum(x,y) = sum(y,x)). 5 [] (sum(x,prod(y,z)) = prod(sum(x,y),sum(x,z))). 7 [] (prod(x,sum(y,z)) = sum(prod(x,y),prod(x,z))). 10 [] (prod(x,comp(x)) = 0). 13 [] (sum(0,x) = x). 14 [] (prod(x,1) = x). 16 [] (sum(a,1) != 1). 23 [] (prod(x,comp(x)) = 0). 25 [] (sum(x,0) = x). 47 [para_into,16,2] (sum(1,a) != 1). 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). 124 [para_from,89,5,demod,25,25] (prod(sum(x,y),x) = x). 154 [para_into,124,14] (sum(1,x) = 1). 160 [binary,154,47] . ------------ end of proof ------------- ------------- memory usage ------------ 4 mallocs of 32700 bytes each (127.7+ K) type (bytes each) gets frees in use avail bytes -------------- statistics ------------- clauses input 28 clauses given 18 clauses generated 405 demod & eval rewrites 624 tautologies deleted 0 clauses forward subsumed 319 (subsumed by sos) 17 clauses kept 87 new demodulators 45 empty clauses 1 clauses back subsumed 1 clauses not processed 9 ----------- times (seconds) ----------- run time 11.41 (run time 0 hr, 0 min, 11 sec) input time 0.87 clausify time 0.00 para_into time 0.48 para_from time 0.60 pre_process time 8.25 demod time 3.56 for_sub time 1.08 renumber time 0.39 cl integrate 0.35 print_cl time 0.88 post_process time 0.74 conflict time 0.07 back_sub time 0.48 FPA build time 0.44 IS build time 0.13 weigh cl time 0.06 window time 0.00