============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 20527 was started by zalta on mally, Fri Jul 27 14:59:38 2007 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). (all x all y (Object(x) & Object(y) -> Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | x = y)). end_of_list. formulas(goals). (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y = x))))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 2 (all x all y (Object(x) & Object(y) -> Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | x = y)) # label(non_clause). [assumption]. 3 (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y = x))))) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. -Object(x) | -Object(y) | Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | y = x. [clausify(2)]. Object(c1). [deny(3)]. Ex1(none_greater,c1). [deny(3)]. -Object(x) | -Ex1(none_greater,x) | Object(f2(x)). [deny(3)]. -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,f2(x)). [deny(3)]. -Object(x) | -Ex1(none_greater,x) | f2(x) != x. [deny(3)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Object, Ex1, Ex2 ]). Function symbol precedence: function_order([ none_greater, conceivable, greater_than, c1, f1, f2 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(positive_inference). % (non-Horn) % set(positive_inference) -> assign(literal_selection, maximal_negative). % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 4 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. 5 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. 6 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. 7 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. 8 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. 9 -Object(x) | -Object(y) | Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | y = x. [clausify(2)]. 10 Object(c1). [deny(3)]. 11 Ex1(none_greater,c1). [deny(3)]. 12 -Object(x) | -Ex1(none_greater,x) | Object(f2(x)). [deny(3)]. 13 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,f2(x)). [deny(3)]. 14 -Object(x) | -Ex1(none_greater,x) | f2(x) != x. [deny(3)]. 15 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(5,a,c)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=8): 4 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. given #2 (I,wt=14): 5 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. given #3 (I,wt=11): 6 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f1(x)). [clausify(1)]. given #4 (I,wt=13): 7 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). [clausify(1)]. given #5 (I,wt=12): 8 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). [clausify(1)]. given #6 (I,wt=15): 9 -Object(x) | -Object(y) | Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | y = x. [clausify(2)]. given #7 (I,wt=2): 10 Object(c1). [deny(3)]. given #8 (I,wt=3): 11 Ex1(none_greater,c1). [deny(3)]. given #9 (I,wt=8): 12 -Object(x) | -Ex1(none_greater,x) | Object(f2(x)). [deny(3)]. given #10 (I,wt=9): 13 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,f2(x)). [deny(3)]. given #11 (I,wt=9): 14 -Object(x) | -Ex1(none_greater,x) | f2(x) != x. [deny(3)]. given #12 (I,wt=12): 15 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(5,a,c)]. given #13 (A,wt=13): 16 -Object(x) | Ex2(greater_than,x,c1) | Ex2(greater_than,c1,x) | c1 = x. [resolve(10,a,9,b)]. given #14 (F,wt=4): 20 f2(c1) != c1. [resolve(14,b,11,a),unit_del(a,10)]. given #15 (T,wt=3): 17 Ex1(conceivable,c1). [resolve(11,a,4,b),unit_del(a,10)]. given #16 (T,wt=3): 18 Object(f2(c1)). [resolve(12,b,11,a),unit_del(a,10)]. given #17 (T,wt=4): 19 Ex1(none_greater,f2(c1)). [resolve(13,b,11,a),unit_del(a,10)]. given #18 (T,wt=4): 26 Object(f2(f2(c1))). [resolve(19,a,12,b),unit_del(a,18)]. given #19 (A,wt=4): 21 -Ex2(greater_than,c1,c1). [ur(15,a,10,a,b,11,a,d,17,a)]. given #20 (F,wt=5): 28 -Ex2(greater_than,c1,f2(c1)). [ur(5,a,18,a,b,19,a,c,10,a,e,17,a)]. given #21 (F,wt=6): 24 f2(f2(c1)) != f2(c1). [resolve(19,a,14,b),unit_del(a,18)]. given #22 (T,wt=4): 27 Ex1(conceivable,f2(c1)). [resolve(19,a,4,b),unit_del(a,18)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 21. % Level of proof is 5. % Maximum clause weight is 15. % Given clauses 22. 1 (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 2 (all x all y (Object(x) & Object(y) -> Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | x = y)) # label(non_clause). [assumption]. 3 (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y = x))))) # label(non_clause) # label(goal). [goal]. 4 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(1)]. 5 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(1)]. 9 -Object(x) | -Object(y) | Ex2(greater_than,x,y) | Ex2(greater_than,y,x) | y = x. [clausify(2)]. 10 Object(c1). [deny(3)]. 11 Ex1(none_greater,c1). [deny(3)]. 12 -Object(x) | -Ex1(none_greater,x) | Object(f2(x)). [deny(3)]. 13 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,f2(x)). [deny(3)]. 14 -Object(x) | -Ex1(none_greater,x) | f2(x) != x. [deny(3)]. 16 -Object(x) | Ex2(greater_than,x,c1) | Ex2(greater_than,c1,x) | c1 = x. [resolve(10,a,9,b)]. 17 Ex1(conceivable,c1). [resolve(11,a,4,b),unit_del(a,10)]. 18 Object(f2(c1)). [resolve(12,b,11,a),unit_del(a,10)]. 19 Ex1(none_greater,f2(c1)). [resolve(13,b,11,a),unit_del(a,10)]. 20 f2(c1) != c1. [resolve(14,b,11,a),unit_del(a,10)]. 22 Ex2(greater_than,f2(c1),c1) | Ex2(greater_than,c1,f2(c1)). [resolve(18,a,16,a),flip(c),unit_del(c,20)]. 27 Ex1(conceivable,f2(c1)). [resolve(19,a,4,b),unit_del(a,18)]. 28 -Ex2(greater_than,c1,f2(c1)). [ur(5,a,18,a,b,19,a,c,10,a,e,17,a)]. 29 Ex2(greater_than,f2(c1),c1). [back_unit_del(22),unit_del(b,28)]. 33 $F. [ur(5,a,10,a,b,11,a,c,18,a,e,27,a),unit_del(a,29)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=49. Kept=29. proofs=1. Usable=22. Sos=5. Demods=0. Limbo=1, Disabled=12. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=19. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=9. Nonunit_bsub_feature_tests=17. Megabytes=0.05. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 20527 exit (max_proofs) Fri Jul 27 14:59:38 2007