--------- OTTER 1.03+, 1989 --------- Job run on Wed Aug 9 11:15:03 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,sum(a,b)) != a). 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 9.47 sec ----> 131 [binary,127,83] . ---------------- 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). 16 [] (prod(a,sum(a,b)) != a). 17 [] (sum(x,y) = sum(y,x)). 18 [] (prod(x,y) = prod(y,x)). 23 [] (prod(x,comp(x)) = 0). 25 [] (sum(x,0) = x). 65 [para_from,10,7,demod,25] (prod(x,sum(y,comp(x))) = prod(x,y)). 83 [para_into,16,2,demod,17,18] (prod(sum(a,b),a) != a). 90 [para_into,65,13,demod,23] (prod(x,0) = 0). 127 [para_from,90,5,demod,25,25] (prod(sum(x,y),x) = x). 131 [binary,127,83] . ------------ 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 15 clauses generated 314 demod & eval rewrites 505 tautologies deleted 0 clauses forward subsumed 243 (subsumed by sos) 20 clauses kept 72 new demodulators 31 empty clauses 1 clauses back subsumed 0 clauses not processed 3 ----------- times (seconds) ----------- run time 9.72 (run time 0 hr, 0 min, 9 sec) input time 0.82 clausify time 0.00 para_into time 0.35 para_from time 0.55 pre_process time 6.95 demod time 3.03 for_sub time 0.94 renumber time 0.41 cl integrate 0.25 print_cl time 0.83 post_process time 0.62 conflict time 0.14 back_sub time 0.29 FPA build time 0.30 IS build time 0.15 weigh cl time 0.07 window time 0.00