% problem-set/pelletier/p44.out % created : 08/17/89 % revised : 08/17/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Aug 17 14:40:44 1989 set(hyper_res). set(ur_res). set(simplify_fol). -------> sos clausifies to: list(sos). 1 [] -F(x) | G(f1(x)). 2 [] -F(x) | H(x,f1(x)). 3 [] -F(x) | G(f2(x)). 4 [] -F(x) | -H(x,f2(x)). 5 [] J(c1). 6 [] -G(y) | H(c1,y). 7 [] -J(x) | F(x). end_of_list. -----> EMPTY CLAUSE at 0.23 sec ----> 13 [hyper,4,8,11] . ---------------- PROOF ---------------- 3 [] -F(x) | G(f2(x)). 4 [] -F(x) | -H(x,f2(x)). 5 [] J(c1). 6 [] -G(y) | H(c1,y). 7 [] -J(x) | F(x). 8 [hyper,7,5] F(c1). 10 [hyper,3,8] G(f2(c1)). 11 [hyper,6,10] H(c1,f2(c1)). 13 [hyper,4,8,11] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 0 clauses given 12 clauses generated 13 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 7 (subsumed by sos) 5 clauses kept 6 empty clauses 1 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.34 (run time 0 hr, 0 min, 0 sec) input time 0.12 clausify time 0.03 hyper_res time 0.01 UR_res time 0.01 pre_process time 0.03 demod time 0.00 lex_rpo time 0.00 for_sub time 0.01 renumber time 0.00 cl integrate 0.00 print_cl time 0.01 post_process time 0.03 conflict time 0.00 back_sub time 0.00 FPA build time 0.01 IS build time 0.00 weigh cl time 0.00 lex_rpo time 0.00 window time 0.00