% problem-set/algebra/henkin.models/hp5.ver2.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 08:14:38 1989 set(ur_res). set(para_from). set(para_from_left). set(para_from_right). set(para_into). 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). 9 [] (f(x,1) = 0). 10 [] (f(0,x) = 0). end_of_list. list(sos). 11 [] LE(a,b). 12 [] LE(b,c). 13 [] -LE(a,c). end_of_list. list(demodulators). 14 [] (f(x,1) = 0). 15 [] (f(0,x) = 0). end_of_list. new given clause: 11 [] LE(a,b). ** KEPT: 16 [ur,11,2] (f(a,b) = 0). new given clause: 12 [] LE(b,c). ** KEPT: 17 [ur,12,2] (f(b,c) = 0). new given clause: 13 [] -LE(a,c). ** KEPT: 18 [ur,13,3] (f(a,c) != 0). new given clause: 16 [ur,11,2] (f(a,b) = 0). ** KEPT: 19 [para_into,16,2] (f(a,b) = f(x,y)) | -LE(x,y). ** KEPT: 20 [para_from,16,5,demod,15] LE(f(f(a,x),f(b,x)),0). ** KEPT: 21 [para_from,16,5] LE(f(f(x,b),0),f(f(x,a),b)). ** KEPT: 22 [para_from,16,10,demod,15] (0 = f(a,b)). ** KEPT: 23 [para_from,16,10] (f(f(a,b),x) = 0). ** KEPT: 24 [para_from,16,6] LE(f(a,b),x). ** KEPT: 25 [para_from,16,3] (f(x,y) != f(a,b)) | LE(x,y). ** KEPT: 26 [para_from,16,2] -LE(x,y) | (f(x,y) = f(a,b)). new given clause: 17 [ur,12,2] (f(b,c) = 0). ** KEPT: 27 [para_into,17,16] (f(b,c) = f(a,b)). ** KEPT: 28 [para_into,17,2] (f(b,c) = f(x,y)) | -LE(x,y). ** KEPT: 29 [para_from,17,5,demod,15] LE(f(f(b,x),f(c,x)),0). ** KEPT: 30 [para_from,17,5] LE(f(f(x,c),0),f(f(x,b),c)). ** KEPT: 31 [para_from,17,16] (f(a,b) = f(b,c)). ** KEPT: 32 [para_from,17,10,demod,15] (0 = f(b,c)). ** KEPT: 33 [para_from,17,10] (f(f(b,c),x) = 0). ** KEPT: 34 [para_from,17,6] LE(f(b,c),x). ** KEPT: 35 [para_from,17,3] (f(x,y) != f(b,c)) | LE(x,y). ** KEPT: 36 [para_from,17,2] -LE(x,y) | (f(x,y) = f(b,c)). new given clause: 18 [ur,13,3] (f(a,c) != 0). ** KEPT: 37 [ur,18,7,6] -LE(f(a,c),0). ** KEPT: 38 [para_into,18,17] (f(a,c) != f(b,c)). ** KEPT: 39 [para_into,18,16] (f(a,c) != f(a,b)). ** KEPT: 40 [para_into,18,2] (f(a,c) != f(x,y)) | -LE(x,y). new given clause: 22 [para_from,16,10,demod,15] (0 = f(a,b)). new given clause: 24 [para_from,16,6] LE(f(a,b),x). ** KEPT: 41 [ur,24,7,4] (f(f(a,b),x) = f(a,b)). ** KEPT: 42 [ur,24,7,4] (f(a,b) = f(f(a,b),x)). new given clause: 32 [para_from,17,10,demod,15] (0 = f(b,c)). new given clause: 34 [para_from,17,6] LE(f(b,c),x). ** KEPT: 43 [ur,34,7,4] (f(f(b,c),x) = f(b,c)). ** KEPT: 44 [ur,34,7,4] (f(b,c) = f(f(b,c),x)). new given clause: 37 [ur,18,7,6] -LE(f(a,c),0). ** KEPT: 45 [ur,37,3] (f(f(a,c),0) != 0). ** KEPT: 46 [para_into,37,32] -LE(f(a,c),f(b,c)). ** KEPT: 47 [para_into,37,22] -LE(f(a,c),f(a,b)). ** KEPT: 48 [para_into,37,2] -LE(f(a,c),f(x,y)) | -LE(x,y). new given clause: 23 [para_from,16,10] (f(f(a,b),x) = 0). ** KEPT: 49 [para_into,23,23] (f(f(a,b),x) = f(f(a,b),y)). ** KEPT: 50 [para_into,23,32] (f(f(a,b),x) = f(b,c)). ** KEPT: 51 [para_into,23,2] (f(f(a,b),x) = f(y,z)) | -LE(y,z). ** KEPT: 52 [para_from,23,5,demod,15] LE(f(f(f(a,b),x),f(y,x)),0). ** KEPT: 53 [para_from,23,5] LE(f(f(x,y),0),f(f(x,f(a,b)),y)). ** KEPT: 54 [para_from,23,17] (f(b,c) = f(f(a,b),x)). ** KEPT: 55 [para_from,23,10,demod,15] (0 = f(f(a,b),x)). ** KEPT: 56 [para_from,23,37] -LE(f(a,c),f(f(a,b),x)). ** KEPT: 57 [para_from,23,18] (f(a,c) != f(f(a,b),x)). ** KEPT: 58 [para_from,23,10] (f(f(f(a,b),x),y) = 0). ** KEPT: 59 [para_from,23,6] LE(f(f(a,b),x),y). ** KEPT: 60 [para_from,23,3] (f(x,y) != f(f(a,b),z)) | LE(x,y). ** KEPT: 61 [para_from,23,2] -LE(x,y) | (f(x,y) = f(f(a,b),z)). new given clause: 27 [para_into,17,16] (f(b,c) = f(a,b)). ** KEPT: 62 [para_from,27,5] LE(f(f(b,x),f(c,x)),f(f(a,b),x)). ** KEPT: 63 [para_from,27,5] LE(f(f(x,c),f(a,b)),f(f(x,b),c)). ** KEPT: 64 [para_from,27,5] LE(f(f(a,x),f(b,x)),f(f(b,c),x)). ** KEPT: 65 [para_from,27,5] LE(f(f(x,b),f(b,c)),f(f(x,a),b)). ** KEPT: 66 [para_from,27,5] LE(f(f(b,c),f(x,b)),f(f(a,x),b)). new given clause: 31 [para_from,17,16] (f(a,b) = f(b,c)). new given clause: 33 [para_from,17,10] (f(f(b,c),x) = 0). ** KEPT: 67 [para_into,33,33] (f(f(b,c),x) = f(f(b,c),y)). ** KEPT: 68 [para_into,33,23] (f(f(b,c),x) = f(f(a,b),y)). ** KEPT: 69 [para_into,33,22] (f(f(b,c),x) = f(a,b)). ** KEPT: 70 [para_into,33,2] (f(f(b,c),x) = f(y,z)) | -LE(y,z). ** KEPT: 71 [para_from,33,5,demod,15] LE(f(f(f(b,c),x),f(y,x)),0). ** KEPT: 72 [para_from,33,5] LE(f(f(x,y),0),f(f(x,f(b,c)),y)). ** KEPT: 73 [para_from,33,23] (f(f(a,b),x) = f(f(b,c),y)). ** KEPT: 74 [para_from,33,16] (f(a,b) = f(f(b,c),x)). ** KEPT: 75 [para_from,33,10,demod,15] (0 = f(f(b,c),x)). ** KEPT: 76 [para_from,33,37] -LE(f(a,c),f(f(b,c),x)). ** KEPT: 77 [para_from,33,18] (f(a,c) != f(f(b,c),x)). ** KEPT: 78 [para_from,33,10] (f(f(f(b,c),x),y) = 0). ** KEPT: 79 [para_from,33,6] LE(f(f(b,c),x),y). ** KEPT: 80 [para_from,33,3] (f(x,y) != f(f(b,c),z)) | LE(x,y). ** KEPT: 81 [para_from,33,2] -LE(x,y) | (f(x,y) = f(f(b,c),z)). 79 back subsumes: 66 [para_from,27,5] LE(f(f(b,c),f(x,b)),f(f(a,x),b)). new given clause: 38 [para_into,18,17] (f(a,c) != f(b,c)). new given clause: 39 [para_into,18,16] (f(a,c) != f(a,b)). new given clause: 45 [ur,37,3] (f(f(a,c),0) != 0). ** KEPT: 82 [ur,45,7,6] -LE(f(f(a,c),0),0). ** KEPT: 83 [para_into,45,33] (f(f(a,c),f(f(b,c),x)) != 0). ** KEPT: 84 [para_into,45,23] (f(f(a,c),f(f(a,b),x)) != 0). ** KEPT: 85 [para_into,45,32] (f(f(a,c),f(b,c)) != 0). ** KEPT: 86 [para_into,45,22] (f(f(a,c),f(a,b)) != 0). ** KEPT: 87 [para_into,45,2] (f(f(a,c),f(x,y)) != 0) | -LE(x,y). ** KEPT: 88 [para_into,45,33] (f(f(a,c),0) != f(f(b,c),x)). ** KEPT: 89 [para_into,45,23] (f(f(a,c),0) != f(f(a,b),x)). ** KEPT: 90 [para_into,45,32] (f(f(a,c),0) != f(b,c)). ** KEPT: 91 [para_into,45,22] (f(f(a,c),0) != f(a,b)). ** KEPT: 92 [para_into,45,2] (f(f(a,c),0) != f(x,y)) | -LE(x,y). new given clause: 46 [para_into,37,32] -LE(f(a,c),f(b,c)). new given clause: 47 [para_into,37,22] -LE(f(a,c),f(a,b)). new given clause: 55 [para_from,23,10,demod,15] (0 = f(f(a,b),x)). new given clause: 59 [para_from,23,6] LE(f(f(a,b),x),y). ** KEPT: 93 [ur,59,7,5] (f(f(a,x),f(b,x)) = f(f(a,b),x)). ** KEPT: 94 [ur,59,7,4] (f(f(f(a,b),x),y) = f(f(a,b),x)). ** KEPT: 95 [ur,59,7,5] (f(f(a,b),x) = f(f(a,x),f(b,x))). ** KEPT: 96 [ur,59,7,4] (f(f(a,b),x) = f(f(f(a,b),x),y)). new given clause: 75 [para_from,33,10,demod,15] (0 = f(f(b,c),x)). new given clause: 79 [para_from,33,6] LE(f(f(b,c),x),y). ** KEPT: 97 [ur,79,7,5] (f(f(b,x),f(c,x)) = f(f(b,c),x)). ** KEPT: 98 [ur,79,7,4] (f(f(f(b,c),x),y) = f(f(b,c),x)). ** KEPT: 99 [ur,79,7,5] (f(f(b,c),x) = f(f(b,x),f(c,x))). ** KEPT: 100 [ur,79,7,4] (f(f(b,c),x) = f(f(f(b,c),x),y)). new given clause: 82 [ur,45,7,6] -LE(f(f(a,c),0),0). ** KEPT: 101 [ur,82,3] (f(f(f(a,c),0),0) != 0). ** KEPT: 102 [para_into,82,75] -LE(f(f(a,c),f(f(b,c),x)),0). ** KEPT: 103 [para_into,82,55] -LE(f(f(a,c),f(f(a,b),x)),0). ** KEPT: 104 [para_into,82,32] -LE(f(f(a,c),f(b,c)),0). ** KEPT: 105 [para_into,82,22] -LE(f(f(a,c),f(a,b)),0). ** KEPT: 106 [para_into,82,2] -LE(f(f(a,c),f(x,y)),0) | -LE(x,y). ** KEPT: 107 [para_into,82,75] -LE(f(f(a,c),0),f(f(b,c),x)). ** KEPT: 108 [para_into,82,55] -LE(f(f(a,c),0),f(f(a,b),x)). ** KEPT: 109 [para_into,82,32] -LE(f(f(a,c),0),f(b,c)). ** KEPT: 110 [para_into,82,22] -LE(f(f(a,c),0),f(a,b)). ** KEPT: 111 [para_into,82,2] -LE(f(f(a,c),0),f(x,y)) | -LE(x,y). ----> UNIT CONFLICT at 4.22 sec ----> 112 [binary,104,20] . ---------------- PROOF ---------------- 2 [] -LE(x,y) | (f(x,y) = 0). 3 [] (f(x,y) != 0) | LE(x,y). 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). 10 [] (f(0,x) = 0). 11 [] LE(a,b). 12 [] LE(b,c). 13 [] -LE(a,c). 15 [] (f(0,x) = 0). 16 [ur,11,2] (f(a,b) = 0). 17 [ur,12,2] (f(b,c) = 0). 18 [ur,13,3] (f(a,c) != 0). 20 [para_from,16,5,demod,15] LE(f(f(a,x),f(b,x)),0). 32 [para_from,17,10,demod,15] (0 = f(b,c)). 37 [ur,18,7,6] -LE(f(a,c),0). 45 [ur,37,3] (f(f(a,c),0) != 0). 82 [ur,45,7,6] -LE(f(f(a,c),0),0). 104 [para_into,82,32] -LE(f(f(a,c),f(b,c)),0). 112 [binary,104,20] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 15 clauses given 25 clauses generated 501 demod & eval rewrites 80 tautologies deleted 0 clauses forward subsumed 405 (subsumed by sos) 151 clauses kept 97 empty clauses 1 clauses back subsumed 1 clauses not processed 11 ----------- times (seconds) ----------- run time 4.38 (run time 0 hr, 0 min, 4 sec) input time 0.19 clausify time 0.00 UR_res time 0.19 para_into time 0.33 para_from time 0.30 pre_process time 2.51 demod time 0.57 lex_rpo time 0.00 for_sub time 0.81 renumber time 0.05 cl integrate 0.11 print_cl time 0.38 post_process time 0.48 conflict time 0.20 back_sub time 0.15 FPA build time 0.21 IS build time 0.07 weigh cl time 0.03 window time 0.00