% problem-set/algebra/henkin.models/new.ver1.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 08:17:54 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)). 20 [] P(x,0,x). end_of_list. list(sos). 21 [] -LE(a,a). end_of_list. new given clause: 21 [] -LE(a,a). ** KEPT: 22 [ur,21,17,7] (1 != a). ** KEPT: 23 [ur,21,16,5] (0 != a). ** KEPT: 24 [ur,21,4,20,20,20,20] -P(a,0,a). ** KEPT: 25 [ur,21,4,20,20,20,20] -P(0,0,0). ** KEPT: 26 [ur,21,4,20,20,8,20] -P(f(a,0),0,a). ** KEPT: 27 [ur,21,4,20,8,20,20] -P(a,f(0,0),a). ** KEPT: 28 [ur,21,4,20,8,8,20] -P(f(a,0),f(0,0),a). ** KEPT: 29 [ur,21,3] -P(a,x,a). ** KEPT: 30 [ur,21,2] -P(a,a,0). ----> UNIT CONFLICT at 0.58 sec ----> 31 [binary,24,20] . ---------------- PROOF ---------------- 4 [] -P(x,y,v1) | -P(y,z,v2) | -P(x,z,v3) | -P(v3,v2,v4) | -P(v1,z,v5) | LE(v4,v5). 20 [] P(x,0,x). 21 [] -LE(a,a). 24 [ur,21,4,20,20,20,20] -P(a,0,a). 31 [binary,24,20] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 21 clauses given 1 clauses generated 15 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 6 (subsumed by sos) 4 clauses kept 10 empty clauses 1 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.73 (run time 0 hr, 0 min, 0 sec) input time 0.31 clausify time 0.00 UR_res time 0.13 pre_process time 0.13 demod time 0.00 lex_rpo time 0.00 for_sub time 0.07 renumber time 0.00 cl integrate 0.01 print_cl time 0.03 post_process time 0.03 conflict time 0.00 back_sub time 0.00 FPA build time 0.06 IS build time 0.02 weigh cl time 0.00 window time 0.00