============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 8128 was started by zalta on mally, Tue Jul 24 18:05:40 2007 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all x (object(x) -> -relation1(x))). (all x all F (exemplifies1(F,x) -> relation1(F) & object(x))). (all x all F (is_the(x,F) -> relation1(F) & object(x))). (all F all x (relation1(F) & object(x) -> (is_the(x,F) <-> exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x)))))). end_of_list. formulas(goals). (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x (object(x) -> -relation1(x))) # label(non_clause). [assumption]. 2 (all x all F (exemplifies1(F,x) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 3 (all x all F (is_the(x,F) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 4 (all F all x (relation1(F) & object(x) -> (is_the(x,F) <-> exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x)))))) # label(non_clause). [assumption]. 5 (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))) # 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) | -relation1(x). [clausify(1)]. -exemplifies1(x,y) | relation1(x). [clausify(2)]. -exemplifies1(x,y) | object(y). [clausify(2)]. -is_the(x,y) | relation1(y). [clausify(3)]. -is_the(x,y) | object(x). [clausify(3)]. -relation1(x) | -object(y) | -is_the(y,x) | exemplifies1(x,y). [clausify(4)]. -relation1(x) | -object(y) | -is_the(y,x) | -object(z) | -exemplifies1(x,z) | z = y. [clausify(4)]. -relation1(x) | -object(y) | is_the(y,x) | -exemplifies1(x,y) | object(f1(x,y)). [clausify(4)]. -relation1(x) | -object(y) | is_the(y,x) | -exemplifies1(x,y) | exemplifies1(x,f1(x,y)). [clausify(4)]. -relation1(x) | -object(y) | is_the(y,x) | -exemplifies1(x,y) | f1(x,y) != y. [clausify(4)]. relation1(c1). [deny(5)]. object(c2). [deny(5)]. is_the(c2,c1). [deny(5)]. object(c3). [deny(5)]. is_the(c3,c1). [deny(5)]. -exemplifies1(c1,c3). [deny(5)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating relation1/1 6 -exemplifies1(x,y) | relation1(x). [clausify(2)]. 7 -object(x) | -relation1(x). [clausify(1)]. Derived: -exemplifies1(x,y) | -object(x). [resolve(6,b,7,b)]. 8 -is_the(x,y) | relation1(y). [clausify(3)]. Derived: -is_the(x,y) | -object(y). [resolve(8,b,7,b)]. 9 -relation1(x) | -object(y) | -is_the(y,x) | exemplifies1(x,y). [clausify(4)]. Derived: -object(x) | -is_the(x,y) | exemplifies1(y,x) | -exemplifies1(y,z). [resolve(9,a,6,b)]. Derived: -object(x) | -is_the(x,y) | exemplifies1(y,x) | -is_the(z,y). [resolve(9,a,8,b)]. 10 -relation1(x) | -object(y) | -is_the(y,x) | -object(z) | -exemplifies1(x,z) | z = y. [clausify(4)]. Derived: -object(x) | -is_the(x,y) | -object(z) | -exemplifies1(y,z) | z = x | -exemplifies1(y,u). [resolve(10,a,6,b)]. 11 -relation1(x) | -object(y) | is_the(y,x) | -exemplifies1(x,y) | object(f1(x,y)). [clausify(4)]. Derived: -object(x) | is_the(x,y) | -exemplifies1(y,x) | object(f1(y,x)) | -exemplifies1(y,z). [resolve(11,a,6,b)]. 12 -relation1(x) | -object(y) | is_the(y,x) | -exemplifies1(x,y) | exemplifies1(x,f1(x,y)). [clausify(4)]. Derived: -object(x) | is_the(x,y) | -exemplifies1(y,x) | exemplifies1(y,f1(y,x)) | -exemplifies1(y,z). [resolve(12,a,6,b)]. 13 -relation1(x) | -object(y) | is_the(y,x) | -exemplifies1(x,y) | f1(x,y) != y. [clausify(4)]. Derived: -object(x) | is_the(x,y) | -exemplifies1(y,x) | f1(y,x) != x | -exemplifies1(y,z). [resolve(13,a,6,b)]. 14 relation1(c1). [deny(5)]. Derived: -object(c1). [resolve(14,a,7,b)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, object, exemplifies1, is_the ]). Function symbol precedence: function_order([ c1, c2, c3, f1 ]). 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). 15 -exemplifies1(x,y) | object(y). [clausify(2)]. 16 -is_the(x,y) | object(x). [clausify(3)]. 17 object(c2). [deny(5)]. 18 is_the(c2,c1). [deny(5)]. 19 object(c3). [deny(5)]. 20 is_the(c3,c1). [deny(5)]. 21 -exemplifies1(c1,c3). [deny(5)]. 22 -exemplifies1(x,y) | -object(x). [resolve(6,b,7,b)]. 23 -is_the(x,y) | -object(y). [resolve(8,b,7,b)]. 30 -object(c1). [resolve(14,a,7,b)]. 31 -object(x) | -is_the(x,y) | exemplifies1(y,x). [factor(25,b,d)]. 32 -object(x) | -is_the(x,y) | -object(z) | -exemplifies1(y,z) | z = x. [factor(26,d,f)]. 33 -object(x) | is_the(x,y) | -exemplifies1(y,x) | object(f1(y,x)). [factor(27,c,e)]. 34 -object(x) | is_the(x,y) | -exemplifies1(y,x) | exemplifies1(y,f1(y,x)). [factor(28,c,e)]. 35 -object(x) | is_the(x,y) | -exemplifies1(y,x) | f1(y,x) != x. [factor(29,c,e)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 15 -exemplifies1(x,y) | object(y). [clausify(2)]. given #2 (I,wt=5): 16 -is_the(x,y) | object(x). [clausify(3)]. given #3 (I,wt=2): 17 object(c2). [deny(5)]. given #4 (I,wt=3): 18 is_the(c2,c1). [deny(5)]. given #5 (I,wt=2): 19 object(c3). [deny(5)]. given #6 (I,wt=3): 20 is_the(c3,c1). [deny(5)]. given #7 (I,wt=3): 21 -exemplifies1(c1,c3). [deny(5)]. given #8 (I,wt=5): 22 -exemplifies1(x,y) | -object(x). [resolve(6,b,7,b)]. given #9 (I,wt=5): 23 -is_the(x,y) | -object(y). [resolve(8,b,7,b)]. given #10 (I,wt=2): 30 -object(c1). [resolve(14,a,7,b)]. given #11 (I,wt=8): 31 -object(x) | -is_the(x,y) | exemplifies1(y,x). [factor(25,b,d)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 11. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 11. 3 (all x all F (is_the(x,F) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 4 (all F all x (relation1(F) & object(x) -> (is_the(x,F) <-> exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x)))))) # label(non_clause). [assumption]. 5 (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))) # label(non_clause) # label(goal). [goal]. 8 -is_the(x,y) | relation1(y). [clausify(3)]. 9 -relation1(x) | -object(y) | -is_the(y,x) | exemplifies1(x,y). [clausify(4)]. 19 object(c3). [deny(5)]. 20 is_the(c3,c1). [deny(5)]. 21 -exemplifies1(c1,c3). [deny(5)]. 25 -object(x) | -is_the(x,y) | exemplifies1(y,x) | -is_the(z,y). [resolve(9,a,8,b)]. 31 -object(x) | -is_the(x,y) | exemplifies1(y,x). [factor(25,b,d)]. 42 $F. [resolve(31,b,20,a),unit_del(a,19),unit_del(b,21)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=11. Generated=36. Kept=27. proofs=1. Usable=11. Sos=10. Demods=0. Limbo=0, Disabled=31. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=8. Back_subsumed=6. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=16. Nonunit_bsub_feature_tests=30. Megabytes=0.04. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 8128 exit (max_proofs) Tue Jul 24 18:05:40 2007