% problem-set/algebra/henkin.models/hp6.ver1.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 09:51:22 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). end_of_list. list(sos). 24 [] P(a,b,c). 25 [] LE(c,d). 26 [] P(a,d,e). 27 [] -LE(e,b). end_of_list. list(demodulators). 28 [] (f(x,1) = 0). 29 [] (f(0,x) = 0). 30 [] (f(x,x) = 0). 31 [] (f(x,0) = x). end_of_list. ----> UNIT CONFLICT at 386.36 sec ----> 1599 [binary,1598,8] . ---------------- PROOF ---------------- 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). 8 [] P(x,y,f(x,y)). 15 [] (x != y) | -P(w,z,x) | P(w,z,y). 21 [] P(0,x,0). 23 [] P(x,0,x). 24 [] P(a,b,c). 25 [] LE(c,d). 26 [] P(a,d,e). 27 [] -LE(e,b). 32 [hyper,25,1] P(c,d,0). 38 [ur,27,2] -P(e,b,0). 121 [hyper,32,4,24,8,26,8] LE(f(e,f(b,d)),0). 144 [ur,38,15,8] (f(e,b) != 0). 267 [ur,144,6,5] -LE(f(e,b),0). 971 [hyper,121,6,5] (f(e,f(b,d)) = 0). 1467 [hyper,971,15,8] P(e,f(b,d),0). 1512 [ur,1467,4,8,23,21,267] -P(f(b,d),b,0). 1595 [ur,1512,1] -LE(f(b,d),b). 1598 [ur,1595,3] -P(b,x,f(b,d)). 1599 [binary,1598,8] . ------------ end of proof ------------- ------------- memory usage ------------ 15 mallocs of 32700 bytes each (479.0+ K) -------------- statistics ------------- clauses input 31 clauses given 639 clauses generated 26941 demod & eval rewrites 15254 tautologies deleted 0 clauses forward subsumed 25387 (subsumed by sos) 11180 clauses kept 1555 new demodulators 13 empty clauses 1 clauses back subsumed 151 clauses not processed 4 ----------- times (seconds) ----------- run time 386.53 (run time 0 hr, 6 min, 26 sec) input time 0.38 clausify time 0.00 hyper_res time 8.81 UR_res time 224.95 pre_process time 134.60 demod time 29.97 lex_rpo time 0.00 for_sub time 67.13 renumber time 10.16 cl integrate 1.31 print_cl time 5.28 post_process time 9.58 conflict time 4.09 back_sub time 3.19 FPA build time 2.14 IS build time 0.83 weigh cl time 0.42 window time 0.00