% problem-set/algebra/henkin.models/hp7.ver3.out % created : 07/19/89 % revised : 07/19/89 --------- OTTER 1.03+, 1989 --------- Job run on Wed Jul 19 05:49:33 1989 set(ur_res). set(para_from). set(para_from_left). set(para_from_right). set(order_eq). assign(max_seconds,1800). list(axioms). 1 [] (x = x). 2 [] (f(f(x,y),x) = 0). 3 [] (f(f(f(x,z),f(y,z)),f(f(x,y),z)) = 0). 4 [] (f(0,x) = 0). 5 [] (f(x,y) != 0) | (f(y,x) != 0) | (x = y). 6 [] (f(x,1) = 0). 7 [] (f(x,y) != 0) | (f(y,z) != 0) | (f(x,z) = 0). end_of_list. list(sos). 8 [] (f(a,b) = 0). 9 [] (f(f(c,b),f(c,a)) != 0). end_of_list. list(demodulators). 10 [] (f(x,1) = 0). 11 [] (f(0,x) = 0). 12 [] (f(x,x) = 0). 13 [] (f(x,0) = x). end_of_list. ----> UNIT CONFLICT at 1.86 sec ----> 63 [binary,60,18] . ---------------- PROOF ---------------- 2 [] (f(f(x,y),x) = 0). 3 [] (f(f(f(x,z),f(y,z)),f(f(x,y),z)) = 0). 7 [] (f(x,y) != 0) | (f(y,z) != 0) | (f(x,z) = 0). 8 [] (f(a,b) = 0). 9 [] (f(f(c,b),f(c,a)) != 0). 13 [] (f(x,0) = x). 18 [para_from,8,3,demod,13] (f(f(x,b),f(f(x,a),b)) = 0). 60 [ur,9,7,2] (f(f(c,b),f(f(c,a),x)) != 0). 63 [binary,60,18] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 13 clauses given 4 clauses generated 100 demod & eval rewrites 35 tautologies deleted 0 clauses forward subsumed 51 (subsumed by sos) 9 clauses kept 50 empty clauses 1 clauses back subsumed 0 clauses not processed 6 ----------- times (seconds) ----------- run time 2.00 (run time 0 hr, 0 min, 1 sec) input time 0.18 clausify time 0.00 UR_res time 0.11 para_from time 0.11 pre_process time 1.12 demod time 0.17 lex_rpo time 0.00 for_sub time 0.38 renumber time 0.04 cl integrate 0.06 print_cl time 0.20 post_process time 0.32 conflict time 0.09 back_sub time 0.17 FPA build time 0.11 IS build time 0.04 weigh cl time 0.02 window time 0.00