% problem-set/pelletier/p36.out % created : 08/17/89 % revised : 08/17/89 --------- OTTER 1.03+, 1989 --------- Job run on Thu Aug 17 14:52:30 1989 set(hyper_res). set(ur_res). set(factor). set(simplify_fol). -------> sos clausifies to: list(sos). 1 [] F(x,f1(x)). 2 [] G(x,f2(x)). 3 [] -F(x,y) | -F(y,z) | H(x,z). 4 [] -F(x,y) | -G(y,z) | H(x,z). 5 [] -G(x,y) | -F(y,z) | H(x,z). 6 [] -G(x,y) | -G(y,z) | H(x,z). 7 [] -H(c1,y). end_of_list. new given clause: 7 [] -H(c1,y). new given clause: 1 [] F(x,f1(x)). new given clause: 2 [] G(x,f2(x)). new given clause: 3 [] -F(x,y) | -F(y,z) | H(x,z). ** KEPT: 8 [hyper,3,1,1] H(x,f1(f1(x))). ----> UNIT CONFLICT at 0.16 sec ----> 9 [binary,8,7] . ---------------- PROOF ---------------- 1 [] F(x,f1(x)). 3 [] -F(x,y) | -F(y,z) | H(x,z). 7 [] -H(c1,y). 8 [hyper,3,1,1] H(x,f1(f1(x))). 9 [binary,8,7] . ------------ end of proof ------------- ------------- memory usage ------------ 1 mallocs of 32700 bytes each (31.9+ K) -------------- statistics ------------- clauses input 0 clauses given 4 clauses generated 1 (factors generated) 0 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 0 (subsumed by sos) 0 clauses kept 2 empty clauses 1 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 0.27 (run time 0 hr, 0 min, 0 sec) input time 0.14 clausify time 0.03 hyper_res time 0.01 UR_res time 0.00 pre_process time 0.01 demod time 0.00 lex_rpo time 0.00 for_sub time 0.00 renumber time 0.00 cl integrate 0.00 print_cl time 0.00 post_process time 0.02 conflict time 0.00 back_sub time 0.00 factor 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