% problem-set/algebra/henkin.models/hp3.ver3.out % created : 07/19/89 % revised : 07/19/89 --------- OTTER 1.03+, 1989 --------- Job run on Wed Jul 19 05:49:05 1989 set(ur_res). set(para_from_left). set(para_from_right). set(para_into). 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). end_of_list. list(sos). 7 [] (f(a,a) != 0). end_of_list. list(demodulators). 8 [] (f(x,1) = 0). 9 [] (f(0,x) = 0). end_of_list. ----> UNIT CONFLICT at 1.31 sec ----> 41 [binary,38,3] . ---------------- PROOF ---------------- 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). 7 [] (f(a,a) != 0). 10 [ur,7,5,4] (f(f(a,a),0) != 0). 13 [ur,10,5,4] (f(f(f(a,a),0),0) != 0). 20 [para_into,13,2] (f(f(f(a,a),f(f(x,y),x)),0) != 0). 38 [para_into,20,2] (f(f(f(a,a),f(f(x,y),x)),f(f(z,u),z)) != 0). 41 [binary,38,3] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 9 clauses given 8 clauses generated 88 demod & eval rewrites 44 tautologies deleted 0 clauses forward subsumed 57 (subsumed by sos) 5 clauses kept 32 empty clauses 1 clauses back subsumed 0 clauses not processed 5 ----------- times (seconds) ----------- run time 1.44 (run time 0 hr, 0 min, 1 sec) input time 0.14 clausify time 0.00 UR_res time 0.10 para_into time 0.12 pre_process time 0.73 demod time 0.18 lex_rpo time 0.00 for_sub time 0.15 renumber time 0.04 cl integrate 0.05 print_cl time 0.14 post_process time 0.21 conflict time 0.10 back_sub time 0.06 FPA build time 0.06 IS build time 0.03 weigh cl time 0.01 window time 0.00