% problem-set/algebra/henkin.models/hp11.ver2.out % created : 07/19/89 % revised : 07/20/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 10:26:29 1989 set(ur_res). set(para_from). set(para_from_left). set(para_from_right). set(para_into). set(order_eq). set(dynamic_demod). 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). 11 [] (f(x,x) = 0). 12 [] (f(x,0) = x). 13 [] -LE(x,y) | -LE(y,z) | LE(x,z). 14 [] -LE(f(x,y),z) | LE(f(x,z),y). 15 [] -LE(x,y) | LE(f(z,y),f(z,x)). 16 [] -LE(x,y) | LE(f(x,z),f(y,z)). 17 [] (f(1,f(1,f(1,x))) = f(1,x)). 18 [] (f(f(1,x),f(1,f(1,x))) = f(1,x)). end_of_list. list(sos). 19 [] (f(f(1,a),f(1,f(1,b))) != f(f(1,b),f(1,f(1,a)))). 20 [] (f(1,a) = c). 21 [] (f(1,b) = d). 22 [] (f(1,c) = e). 23 [] (f(1,d) = g). 24 [] (f(c,g) != f(d,e)). end_of_list. list(demodulators). 25 [] (f(x,1) = 0). 26 [] (f(0,x) = 0). 27 [] (f(x,x) = 0). 28 [] (f(x,0) = x). 29 [] (f(1,f(1,f(1,x))) = f(1,x)). 30 [] (f(f(1,x),f(1,f(1,x))) = f(1,x)). end_of_list. ----> UNIT CONFLICT at 4349.11 sec ----> 17951 [binary,17945,1587] . ---------------- PROOF ---------------- 4 [] LE(f(x,y),x). 5 [] LE(f(f(x,z),f(y,z)),f(f(x,y),z)). 7 [] -LE(x,y) | -LE(y,x) | (x = y). 13 [] -LE(x,y) | -LE(y,z) | LE(x,z). 14 [] -LE(f(x,y),z) | LE(f(x,z),y). 16 [] -LE(x,y) | LE(f(x,z),f(y,z)). 18 [] (f(f(1,x),f(1,f(1,x))) = f(1,x)). 20 [] (f(1,a) = c). 21 [] (f(1,b) = d). 22 [] (f(1,c) = e). 23 [] (f(1,d) = g). 24 [] (f(c,g) != f(d,e)). 25 [] (f(x,1) = 0). 26 [] (f(0,x) = 0). 28 [] (f(x,0) = x). 43 [para_from,20,5,demod,25,26] LE(f(f(x,a),c),0). 59 [para_from,21,5,demod,25,26] LE(f(f(x,b),d),0). 63 [para_into,22,20] (f(1,f(1,a)) = e). 64 [new_demod,63] (f(1,f(1,a)) = e). 77 [para_from,22,5,demod,25,26] LE(f(f(x,c),e),0). 81 [para_into,23,21] (f(1,f(1,b)) = g). 82 [new_demod,81] (f(1,f(1,b)) = g). 95 [para_from,23,5,demod,25,26] LE(f(f(x,d),g),0). 232 [ur,43,14,demod,28] LE(f(x,a),c). 242 [para_into,232,20] LE(c,c). 248 [para_into,242,20] LE(c,f(1,a)). 279 [para_into,248,18,demod,64] LE(c,f(f(1,a),e)). 470 [ur,59,14,demod,28] LE(f(x,b),d). 480 [para_into,470,21] LE(d,d). 486 [para_into,480,21] LE(d,f(1,b)). 519 [para_into,486,18,demod,82] LE(d,f(f(1,b),g)). 929 [ur,77,14,demod,28] LE(f(x,c),e). 936 [ur,929,14] LE(f(x,e),c). 938 [ur,929,13,4] LE(f(f(x,c),y),e). 1123 [ur,95,14,demod,28] LE(f(x,d),g). 1132 [ur,1123,13,4] LE(f(f(x,d),y),g). 1570 [para_into,279,20] LE(c,f(c,e)). 1578 [ur,1570,7,936] (f(c,e) = c). 1587 [para_from,1578,5] LE(f(c,f(x,e)),f(f(c,x),e)). 2450 [para_into,519,21] LE(d,f(d,g)). 2452 [ur,2450,16] LE(f(d,x),f(f(d,g),x)). 2933 [ur,938,13,5] LE(f(f(x,y),f(c,y)),e). 16366 [ur,2933,13,2452] LE(f(d,f(c,g)),e). 16411 [ur,16366,14] LE(f(d,e),f(c,g)). 16502 [ur,16411,7,24] -LE(f(c,g),f(d,e)). 16581 [ur,16502,14] -LE(f(c,f(d,e)),g). 17945 [ur,16581,13,1132] -LE(f(c,f(d,e)),f(f(x,d),y)). 17951 [binary,17945,1587] . ------------ end of proof ------------- ------------- memory usage ------------ 160 mallocs of 32700 bytes each (5109.4+ K) -------------- statistics ------------- clauses input 30 clauses given 1577 clauses generated 143977 demod & eval rewrites 119757 tautologies deleted 334 clauses forward subsumed 125991 (subsumed by sos) 11258 clauses kept 17653 new demodulators 268 empty clauses 1 clauses back subsumed 9797 clauses not processed 12 ----------- times (seconds) ----------- run time 4349.36 (run time 1 hr, 12 min, 29 sec) input time 0.38 clausify time 0.00 UR_res time 108.74 para_into time 74.43 para_from time 40.98 pre_process time 2894.94 demod time 243.70 lex_rpo time 0.00 for_sub time 2345.25 renumber time 57.76 cl integrate 21.76 print_cl time 69.17 post_process time 1159.39 conflict time 425.51 back_sub time 273.03 FPA build time 25.40 IS build time 12.37 weigh cl time 6.46 window time 0.00