----- Otter 3.2i, February 2003 ----- The process was started by mccune on theorem.mcs.anl.gov, Wed Jul 16 09:50:51 2003 The command was "otter". The process ID is 31150. set(hyper_res). assign(max_given,1). list(usable). 1 [] -major(e(x,y))| -minor(x)|P(y)|minor_instance(x). 2 [] major(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w ,v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)). end_of_list. list(sos). 3 [] minor(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),e( v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=48) 3 [] minor(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)), u)),x)),e(v,e(e(e(v,w),e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10), e(v11,v10)),v11)))). ** KEPT (pick-wt=2940): 4 [hyper,3,1,2] P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u) )),v),e(x,v)))|minor_instance(e(e(e(e(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u) )),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e( u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(e(e(x,e(y ,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e( y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e (e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)) )),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u)) ),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u, z)),u))),v),e(x,v)),x))))),e(x,e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e( x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x, v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))), v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)) ,u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z) ,e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)))))),e(e(e (e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x),e(e(e(e(e(e(x,e(y,e(e(e(y, z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y, e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)) ),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))) ,e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u, z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z ),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z ),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e( e(e(y,z),e(u,z)),u))),v),e(x,v)),x))))),e(x,e(e(e(x,e(y,e(e(e(y,z),e(u,z)), u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)) ,u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z), e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e (y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e (y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)), x)))))),x))),e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y, z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e (e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))), e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))) ,v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z )),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z) ,e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e( e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)))) ),e(x,e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)), u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z), e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e (y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e (y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e( y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))))))),e(e(e(e(e(e(x,e(y,e(e(e(y,z), e(u,z)),u))),v),e(x,v)),x),e(e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e( e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)) ,e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(e(e(x,e(y,e(e(e(y, z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y ,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y, e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e( x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x, v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))), v),e(x,v)),x))))),e(x,e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e (e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e (e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v) ),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e (e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)), u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)))))),x)),e(e(e(e(e( x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x, v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))), v),e(x,v)),x))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z ),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e (e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))) ,e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x ,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e( e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))))),e(x,e(e(e(x,e(y,e(e(e (y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e( e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e (y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e (e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e (x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u) )),v),e(x,v)),x)))))))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),e( e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x),e(e(e(e(e(e(x,e(y,e(e (e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e (e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v) ),x))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)) ,u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z) ,e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e( e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e( e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e (y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))))),e(x,e(e(e(x,e(y,e(e(e(y,z),e(u ,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e( u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e( y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y, e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x) ),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x ,v)),x)))))),x)),e(e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e( e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e (y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u ))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)), u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e (u,z)),u))),v),e(x,v)),x))),e(y,e(e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e( y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e( y,e(e(e(y,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x ))))),e(x,e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u, z)),u))),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y ,z),e(u,z)),u)),e(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x))),e(y,e (e(e(y,z),e(u,z)),u)))),e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),e(e(e(e(x,e(y,e (e(e(y,z),e(u,z)),u))),v),e(x,v)),x)),e(e(y,e(e(e(y,z),e(u,z)),u)),e(e(e(e( x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v)),x)))))))))). Search stopped by max_given option. ============ end of search ============ -------------- statistics ------------- clauses given 1 clauses generated 1 hyper_res generated 1 demod & eval rewrites 0 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 0 (subsumed by sos) 0 unit deletions 0 factor simplifications 0 clauses kept 1 new demodulators 0 empty clauses 0 clauses back demodulated 0 clauses back subsumed 0 usable size 3 sos size 1 demodulators size 0 passive size 0 hot size 0 Kbytes malloced 351 ----------- times (seconds) ----------- user CPU time 0.02 (0 hr, 0 min, 0 sec) system CPU time 0.02 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) input time 0.01 clausify time 0.00 pick given time 0.00 hyper_res time 0.00 pre_process time 0.00 renumber time 0.00 demod time 0.00 order equalities 0.00 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.00 hints keep time 0.00 sort lits time 0.00 forward subsume 0.00 delete cl time 0.00 keep cl time 0.00 hints time 0.00 print_cl time 0.00 conflict time 0.00 new demod time 0.00 post_process time 0.00 back demod time 0.00 back subsume 0.00 factor time 0.00 unindex time 0.00 Process 31150 finished Wed Jul 16 09:50:51 2003