% problem-set/algebra/henkin.models/hp7.ver2.out % created : 07/18/89 % revised : 07/18/89 --------- OTTER 1.03+, 1989 --------- Job run on Tue Jul 18 10:26:14 1989 set(ur_res). set(para_into). set(para_from_left). set(para_from_right). 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). end_of_list. list(sos). 15 [] LE(a,b). 16 [] -LE(f(c,b),f(c,a)). end_of_list. list(demodulators). 17 [] (f(x,1) = 0). 18 [] (f(0,x) = 0). 19 [] (f(x,x) = 0). 20 [] (f(x,0) = x). end_of_list. ----> UNIT CONFLICT at 4.54 sec ----> 121 [binary,120,1] . ---------------- PROOF ---------------- 1 [] (x = x). 3 [] (f(x,y) != 0) | LE(x,y). 13 [] -LE(x,y) | -LE(y,z) | LE(x,z). 14 [] -LE(f(x,y),z) | LE(f(x,z),y). 15 [] LE(a,b). 16 [] -LE(f(c,b),f(c,a)). 19 [] (f(x,x) = 0). 27 [ur,16,14] -LE(f(c,f(c,a)),b). 82 [ur,27,13,15] -LE(f(c,f(c,a)),a). 111 [ur,82,14] -LE(f(c,a),f(c,a)). 120 [ur,111,3,demod,19] (0 != 0). 121 [binary,120,1] . ------------ end of proof ------------- ------------- memory usage ------------ 2 mallocs of 32700 bytes each (63.9+ K) -------------- statistics ------------- clauses input 20 clauses given 49 clauses generated 508 demod & eval rewrites 224 tautologies deleted 0 clauses forward subsumed 411 (subsumed by sos) 16 clauses kept 98 new demodulators 3 empty clauses 1 clauses back subsumed 1 clauses not processed 3 ----------- times (seconds) ----------- run time 4.67 (run time 0 hr, 0 min, 4 sec) input time 0.22 clausify time 0.00 UR_res time 0.49 para_into time 0.34 pre_process time 2.87 demod time 0.49 lex_rpo time 0.00 for_sub time 1.31 renumber time 0.17 cl integrate 0.08 print_cl time 0.29 post_process time 0.35 conflict time 0.14 back_sub time 0.11 FPA build time 0.16 IS build time 0.05 weigh cl time 0.03 window time 0.00