% problem-set/algebra/henkin.models/hp9.ver1.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 10:01:29 1989 set(hyper_res). set(ur_res). set(order_eq). set(dynamic_demod). assign(max_mem,1500). assign(max_seconds,1800). 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,1,0). 21 [] P(0,x,0). 22 [] P(x,x,0). 23 [] P(x,0,x). 24 [] -LE(x,y) | -LE(y,z) | LE(x,z). 25 [] -P(x,y,z) | -LE(z,w) | -P(x,w,v) | LE(v,y). 26 [] -LE(x,y) | -P(z,y,w) | -P(z,x,v) | LE(w,v). 27 [] -LE(x,y) | LE(f(x,z),f(y,z)). end_of_list. list(sos). 28 [] P(1,a,b). 29 [] P(1,b,c). 30 [] P(1,c,d). 31 [] (b != d). end_of_list. list(demodulators). 32 [] (f(x,1) = 0). 33 [] (f(0,x) = 0). 34 [] (f(x,x) = 0). 35 [] (f(x,0) = x). end_of_list. ----> UNIT CONFLICT at 13.03 sec ----> 96 [binary,95,76] . ---------------- 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). 6 [] -LE(x,y) | -LE(y,x) | (x = y). 10 [] (x = x). 12 [] (x != y) | (y != z) | (x = z). 21 [] P(0,x,0). 23 [] P(x,0,x). 25 [] -P(x,y,z) | -LE(z,w) | -P(x,w,v) | LE(v,y). 26 [] -LE(x,y) | -P(z,y,w) | -P(z,x,v) | LE(w,v). 28 [] P(1,a,b). 29 [] P(1,b,c). 30 [] P(1,c,d). 31 [] (b != d). 36 [ur,31,12,10] (d != b). 41 [hyper,28,4,23,21,28,23] LE(b,b). 51 [hyper,29,26,41,29] LE(c,c). 54 [hyper,29,25,28,41] LE(c,a). 72 [hyper,30,26,54,28] LE(b,d). 76 [hyper,30,25,29,51] LE(d,b). 95 [ur,72,6,36] -LE(d,b). 96 [binary,95,76] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 35 clauses given 9 clauses generated 1006 demod & eval rewrites 1039 tautologies deleted 0 clauses forward subsumed 949 (subsumed by sos) 295 clauses kept 58 new demodulators 3 empty clauses 1 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 13.18 (run time 0 hr, 0 min, 13 sec) input time 0.45 clausify time 0.00 hyper_res time 1.64 UR_res time 6.29 pre_process time 4.31 demod time 1.03 lex_rpo time 0.00 for_sub time 2.07 renumber time 0.31 cl integrate 0.04 print_cl time 0.17 post_process time 0.23 conflict time 0.10 back_sub time 0.05 FPA build time 0.12 IS build time 0.04 weigh cl time 0.01 window time 0.00