% problem-set/algebra/henkin.models/hp1.ver3.out % created : 07/19/89 % revised : 07/19/89 --------- OTTER 1.03+, 1989 --------- Job run on Wed Jul 19 05:58:36 1989 set(para_from_left). set(para_from_right). set(para_into). set(order_eq). 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,1) != 0). end_of_list. ----> UNIT CONFLICT at 0.16 sec ----> 13 [binary,8,1] . ---------------- PROOF ---------------- 1 [] (x = x). 6 [] (f(x,1) = 0). 7 [] (f(a,1) != 0). 8 [para_into,7,6] (0 != 0). 13 [binary,8,1] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 7 clauses given 1 clauses generated 5 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 0 (subsumed by sos) 0 clauses kept 6 empty clauses 1 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.27 (run time 0 hr, 0 min, 0 sec) input time 0.11 clausify time 0.00 para_into time 0.01 pre_process time 0.04 demod time 0.00 lex_rpo time 0.00 for_sub time 0.00 renumber time 0.00 cl integrate 0.00 print_cl time 0.01 post_process time 0.01 conflict time 0.00 back_sub time 0.00 FPA build time 0.02 IS build time 0.01 weigh cl time 0.00 window time 0.00