% problem-set/algebra/henkin.models/hp2.ver1.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 08:12:16 1989 set(ur_res). list(axioms). 1 [] -LE(x,y) | P(x,y,0). 2 [] -P(x,y,0) | LE(x,y). 3 [] -P(x,y,z) | LE(z,x). 4 [] -P(x,y,v1) | -P(y,z,v2) | -P(x,z,v3) | -P(v3,v2,v4) | -P(v1,z,v5) | LE(v4,v5). 5 [] LE(0,x). 6 [] -LE(x,y) | -LE(y,x) | (x = y). 7 [] LE(x,1). 8 [] P(x,y,f(x,y)). 9 [] -P(x,y,z) | -P(x,y,w) | (z = w). 10 [] (x = x). 11 [] (x != y) | (y = x). 12 [] (x != y) | (y != z) | (x = z). 13 [] (x != y) | -P(x,w,z) | P(y,w,z). 14 [] (x != y) | -P(w,x,z) | P(w,y,z). 15 [] (x != y) | -P(w,z,x) | P(w,z,y). 16 [] (x != y) | -LE(x,z) | LE(y,z). 17 [] (x != y) | -LE(z,x) | LE(z,y). 18 [] (x != y) | (f(x,w) = f(y,w)). 19 [] (x != y) | (f(w,x) = f(w,y)). end_of_list. list(sos). 20 [] -P(0,a,0). end_of_list. new given clause: 20 [] -P(0,a,0). ** KEPT: 21 [ur,20,15,8] (f(0,a) != 0). ** KEPT: 22 [ur,20,1] -LE(0,a). ----> UNIT CONFLICT at 0.33 sec ----> 23 [binary,22,5] . ---------------- PROOF ---------------- 1 [] -LE(x,y) | P(x,y,0). 5 [] LE(0,x). 20 [] -P(0,a,0). 22 [ur,20,1] -LE(0,a). 23 [binary,22,5] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 20 clauses given 1 clauses generated 5 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 3 (subsumed by sos) 0 clauses kept 3 empty clauses 1 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.45 (run time 0 hr, 0 min, 0 sec) input time 0.27 clausify time 0.00 UR_res time 0.02 pre_process time 0.03 demod time 0.00 lex_rpo time 0.00 for_sub time 0.02 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.05 IS build time 0.01 weigh cl time 0.00 window time 0.00