% problem-set/algebra/henkin.models/new.ver2.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 08:18:07 1989 set(ur_res). list(axioms). 1 [] (x = x). 2 [] -LE(x,y) | (f(x,y) = 0). 3 [] (f(x,y) != 0) | LE(x,y). 4 [] LE(f(x,y),x). 5 [] LE(f(f(x,z),f(y,z)),f(f(x,y),z)). 6 [] LE(0,x). 7 [] -LE(x,y) | -LE(y,x) | (x = y). 8 [] LE(x,1). end_of_list. list(sos). 9 [] -LE(a,a). end_of_list. list(demodulators). 10 [] (f(x,x) = 0). end_of_list. new given clause: 9 [] -LE(a,a). ** KEPT: 11 [ur,9,3,demod,10] (0 != 0). ----> UNIT CONFLICT at 0.16 sec ----> 12 [binary,11,1] . ---------------- PROOF ---------------- 1 [] (x = x). 3 [] (f(x,y) != 0) | LE(x,y). 9 [] -LE(a,a). 10 [] (f(x,x) = 0). 11 [ur,9,3,demod,10] (0 != 0). 12 [binary,11,1] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 10 clauses given 1 clauses generated 1 demod & eval rewrites 1 tautologies deleted 0 clauses forward subsumed 0 (subsumed by sos) 0 clauses kept 2 empty clauses 1 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.30 (run time 0 hr, 0 min, 0 sec) input time 0.14 clausify time 0.00 UR_res time 0.00 pre_process time 0.01 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.00 post_process time 0.02 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