============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 12211 was started by zalta on mally, Thu Oct 9 16:31:16 2008 The command was "prover9". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all F (Relation1(F) -> ((exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))))) -> (exists u (Object(u) & Is_the(u,F)))))). (all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z))))))). (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))). (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). (exists x (Object(x) & Ex1(none_greater,x))). (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))))). (all x (Object(x) -> (Is_the(x,none_greater) & -Ex1(e,x) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). Is_the(g,none_greater). end_of_list. formulas(goals). Ex1(e,g). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all F (Relation1(F) -> ((exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))))) -> (exists u (Object(u) & Is_the(u,F)))))) # label(non_clause). [assumption]. 2 (all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z))))))) # label(non_clause). [assumption]. 3 (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))) # label(non_clause). [assumption]. 4 (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]. 5 (exists x (Object(x) & Ex1(none_greater,x))) # label(non_clause). [assumption]. 6 (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). [assumption]. 7 (all x (Object(x) -> (Is_the(x,none_greater) & -Ex1(e,x) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 8 Ex1(e,g) # 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). -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x)). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x)). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x)). [clausify(1)]. -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x). [clausify(1)]. -Relation1(x) | -Object(y) | -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z). [clausify(2)]. -Is_the(x,y) | Relation1(y). [clausify(3)]. -Is_the(x,y) | Object(x). [clausify(3)]. -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(4)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(4)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f3(x)). [clausify(4)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f3(x),x). [clausify(4)]. -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f3(x)). [clausify(4)]. Object(c1). [clausify(5)]. Ex1(none_greater,c1). [clausify(5)]. -Object(x) | -Ex1(none_greater,x) | Object(c2). [clausify(6)]. -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c2). [clausify(6)]. -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | c2 = y. [clausify(6)]. -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)). [clausify(7)]. -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). [clausify(7)]. -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)). [clausify(7)]. Is_the(g,none_greater). [assumption]. -Ex1(e,g). [deny(8)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating Relation1/1 9 -Is_the(x,y) | Relation1(y). [clausify(3)]. 10 -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x)). [clausify(1)]. 11 -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x). [clausify(1)]. 12 -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x)). [clausify(1)]. 13 -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x). [clausify(1)]. 14 -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x)). [clausify(1)]. 15 -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x). [clausify(1)]. 16 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z). [clausify(2)]. Derived: -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f1(y,z)) | Object(f2(y)). [resolve(9,b,10,a)]. Derived: -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f1(y,z)) | Is_the(f2(y),y). [resolve(9,b,11,a)]. Derived: -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f1(y,z)) | Object(f2(y)). [resolve(9,b,12,a)]. Derived: -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f1(y,z)) | Is_the(f2(y),y). [resolve(9,b,13,a)]. Derived: -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,z) != z | Object(f2(y)). [resolve(9,b,14,a)]. Derived: -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,z) != z | Is_the(f2(y),y). [resolve(9,b,15,a)]. Derived: -Is_the(x,y) | -Object(z) | -Is_the(z,y) | -Object(u) | -Is_the(u,y) | Ex1(y,u). [resolve(9,b,16,a)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Object, Ex1, Is_the, Ex2 ]). Function symbol precedence: function_order([ none_greater, conceivable, e, greater_than, g, c1, c2, f1, f2, f3, f4 ]). 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). 17 -Is_the(x,y) | Object(x). [clausify(3)]. 18 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(4)]. 19 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(4)]. 20 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f3(x)). [clausify(4)]. 21 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f3(x),x). [clausify(4)]. 22 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f3(x)). [clausify(4)]. 23 Object(c1). [clausify(5)]. 24 Ex1(none_greater,c1). [clausify(5)]. 25 -Object(x) | -Ex1(none_greater,x) | Object(c2). [clausify(6)]. 26 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c2). [clausify(6)]. 28 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)). [clausify(7)]. 29 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). [clausify(7)]. 30 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)). [clausify(7)]. 31 Is_the(g,none_greater). [assumption]. 32 -Ex1(e,g). [deny(8)]. 33 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f1(y,z)) | Object(f2(y)). [resolve(9,b,10,a)]. 34 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f1(y,z)) | Is_the(f2(y),y). [resolve(9,b,11,a)]. 35 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f1(y,z)) | Object(f2(y)). [resolve(9,b,12,a)]. 36 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f1(y,z)) | Is_the(f2(y),y). [resolve(9,b,13,a)]. 37 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,z) != z | Object(f2(y)). [resolve(9,b,14,a)]. 38 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,z) != z | Is_the(f2(y),y). [resolve(9,b,15,a)]. 40 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(19,a,c)]. 41 -Object(x) | -Ex1(none_greater,x) | c2 = x. [factor(27,a,c),merge(c)]. 44 -Is_the(x,y) | -Object(x) | Ex1(y,x). [factor(42,a,d),merge(c)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=5): 17 -Is_the(x,y) | Object(x). [clausify(3)]. given #2 (I,wt=8): 18 -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). [clausify(4)]. given #3 (I,wt=14): 19 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(4)]. given #4 (I,wt=11): 20 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f3(x)). [clausify(4)]. given #5 (I,wt=13): 21 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f3(x),x). [clausify(4)]. given #6 (I,wt=12): 22 -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f3(x)). [clausify(4)]. given #7 (I,wt=2): 23 Object(c1). [clausify(5)]. given #8 (I,wt=3): 24 Ex1(none_greater,c1). [clausify(5)]. given #9 (I,wt=7): 25 -Object(x) | -Ex1(none_greater,x) | Object(c2). [clausify(6)]. given #10 (I,wt=8): 26 -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c2). [clausify(6)]. given #11 (I,wt=11): 28 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)). [clausify(7)]. given #12 (I,wt=13): 29 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). [clausify(7)]. given #13 (I,wt=12): 30 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)). [clausify(7)]. given #14 (I,wt=3): 31 Is_the(g,none_greater). [assumption]. given #15 (I,wt=3): 32 -Ex1(e,g). [deny(8)]. given #16 (I,wt=15): 33 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f1(y,z)) | Object(f2(y)). [resolve(9,b,10,a)]. given #17 (I,wt=16): 34 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f1(y,z)) | Is_the(f2(y),y). [resolve(9,b,11,a)]. given #18 (I,wt=16): 35 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f1(y,z)) | Object(f2(y)). [resolve(9,b,12,a)]. given #19 (I,wt=17): 36 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f1(y,z)) | Is_the(f2(y),y). [resolve(9,b,13,a)]. given #20 (I,wt=16): 37 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,z) != z | Object(f2(y)). [resolve(9,b,14,a)]. given #21 (I,wt=17): 38 -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,z) != z | Is_the(f2(y),y). [resolve(9,b,15,a)]. given #22 (I,wt=12): 40 -Object(x) | -Ex1(none_greater,x) | -Ex2(greater_than,x,x) | -Ex1(conceivable,x). [factor(19,a,c)]. given #23 (I,wt=8): 41 -Object(x) | -Ex1(none_greater,x) | c2 = x. [factor(27,a,c),merge(c)]. given #24 (I,wt=8): 44 -Is_the(x,y) | -Object(x) | Ex1(y,x). [factor(42,a,d),merge(c)]. given #25 (A,wt=3): 45 Ex1(conceivable,c1). [resolve(24,a,18,b),unit_del(a,23)]. given #26 (F,wt=4): 64 -Ex2(greater_than,c1,c1). [ur(40,a,23,a,b,24,a,d,45,a)]. given #27 (T,wt=2): 51 Object(g). [resolve(31,a,17,a)]. given #28 (T,wt=3): 52 Object(f4(g)). [back_unit_del(50),unit_del(a,51)]. given #29 (T,wt=3): 61 c2 = c1. [resolve(41,b,24,a),unit_del(a,23)]. given #30 (T,wt=3): 63 Ex1(none_greater,g). [resolve(44,a,31,a),unit_del(a,51)]. given #31 (A,wt=5): 53 Ex2(greater_than,f4(g),g). [back_unit_del(49),unit_del(a,51)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.01) seconds. % Length of proof is 26. % Level of proof is 6. % Maximum clause weight is 16. % Given clauses 31. 2 (all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z))))))) # label(non_clause). [assumption]. 3 (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))) # label(non_clause). [assumption]. 4 (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]. 7 (all x (Object(x) -> (Is_the(x,none_greater) & -Ex1(e,x) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 8 Ex1(e,g) # label(non_clause) # label(goal). [goal]. 9 -Is_the(x,y) | Relation1(y). [clausify(3)]. 16 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z). [clausify(2)]. 17 -Is_the(x,y) | Object(x). [clausify(3)]. 19 -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). [clausify(4)]. 28 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)). [clausify(7)]. 29 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). [clausify(7)]. 30 -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)). [clausify(7)]. 31 Is_the(g,none_greater). [assumption]. 32 -Ex1(e,g). [deny(8)]. 39 -Is_the(x,y) | -Object(z) | -Is_the(z,y) | -Object(u) | -Is_the(u,y) | Ex1(y,u). [resolve(9,b,16,a)]. 42 -Is_the(x,y) | -Object(x) | -Object(z) | -Is_the(z,y) | Ex1(y,z). [factor(39,a,c)]. 44 -Is_the(x,y) | -Object(x) | Ex1(y,x). [factor(42,a,d),merge(c)]. 48 -Object(g) | Ex1(conceivable,f4(g)). [resolve(31,a,30,b),unit_del(b,32)]. 49 -Object(g) | Ex2(greater_than,f4(g),g). [resolve(31,a,29,b),unit_del(b,32)]. 50 -Object(g) | Object(f4(g)). [resolve(31,a,28,b),unit_del(b,32)]. 51 Object(g). [resolve(31,a,17,a)]. 52 Object(f4(g)). [back_unit_del(50),unit_del(a,51)]. 53 Ex2(greater_than,f4(g),g). [back_unit_del(49),unit_del(a,51)]. 54 Ex1(conceivable,f4(g)). [back_unit_del(48),unit_del(a,51)]. 63 Ex1(none_greater,g). [resolve(44,a,31,a),unit_del(a,51)]. 68 $F. [resolve(53,a,19,d),unit_del(a,51),unit_del(b,63),unit_del(c,52),unit_del(d,54)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=31. Generated=64. Kept=51. proofs=1. Usable=28. Sos=11. Demods=1. Limbo=0, Disabled=43. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=12. Back_subsumed=6. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=3. Back_unit_deleted=3. Demod_attempts=80. Demod_rewrites=3. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=10. Nonunit_bsub_feature_tests=52. Megabytes=0.08. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 12211 exit (max_proofs) Thu Oct 9 16:31:16 2008