============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 13273 was started by zalta on mally, Thu Oct 9 22:15:13 2008 The command was "prover9". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all x (Object(x) -> -Relation1(x))). (all x all F (Ex1(F,x) -> Relation1(F) & Object(x))). (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))). (all x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(F,y)))). end_of_list. formulas(goals). (all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z))))))). 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 (Ex1(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 x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(F,y)))) # label(non_clause). [assumption]. 5 (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) # 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)]. -Ex1(x,y) | Relation1(x). [clausify(2)]. -Ex1(x,y) | Object(y). [clausify(2)]. -Is_the(x,y) | Relation1(y). [clausify(3)]. -Is_the(x,y) | Object(x). [clausify(3)]. -Object(x) | -Relation1(y) | -Object(z) | -Is_the(x,y) | z != x | Ex1(y,z). [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)]. -Ex1(c1,c3). [deny(5)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating Relation1/1 6 -Ex1(x,y) | Relation1(x). [clausify(2)]. 7 -Object(x) | -Relation1(x). [clausify(1)]. Derived: -Ex1(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 -Object(x) | -Relation1(y) | -Object(z) | -Is_the(x,y) | z != x | Ex1(y,z). [clausify(4)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Ex1(z,u). [resolve(9,b,6,b)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Is_the(u,z). [resolve(9,b,8,b)]. 10 Relation1(c1). [deny(5)]. Derived: -Object(c1). [resolve(10,a,7,b)]. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 4). % (Horn set with more than one neg. clause) WARNING, because some of the denials share constants, some of the denials or their descendents may be subsumed, preventing the target number of proofs from being found. The shared constants are: c1. Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Object, Is_the, Ex1 ]). Function symbol precedence: function_order([ c1, c2, c3 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=0) % clear(ordered_res). % (HNE depth_diff=0) % set(ur_resolution). % (HNE depth_diff=0) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % 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). 11 -Ex1(x,y) | Object(y). [clausify(2)]. 12 -Is_the(x,y) | Object(x). [clausify(3)]. 13 Object(c2). [deny(5)]. 14 Is_the(c2,c1). [deny(5)]. 15 Object(c3). [deny(5)]. 16 Is_the(c3,c1). [deny(5)]. 17 -Ex1(c1,c3). [deny(5)]. 18 -Ex1(x,y) | -Object(x). [resolve(6,b,7,b)]. 19 -Is_the(x,y) | -Object(y). [resolve(8,b,7,b)]. 20 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Ex1(z,u). [resolve(9,b,6,b)]. 21 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Is_the(u,z). [resolve(9,b,8,b)]. 22 -Object(c1). [resolve(10,a,7,b)]. 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): 11 -Ex1(x,y) | Object(y). [clausify(2)]. given #2 (I,wt=5): 12 -Is_the(x,y) | Object(x). [clausify(3)]. given #3 (I,wt=2): 13 Object(c2). [deny(5)]. given #4 (I,wt=3): 14 Is_the(c2,c1). [deny(5)]. given #5 (I,wt=2): 15 Object(c3). [deny(5)]. given #6 (I,wt=3): 16 Is_the(c3,c1). [deny(5)]. given #7 (I,wt=3): 17 -Ex1(c1,c3). [deny(5)]. given #8 (I,wt=5): 18 -Ex1(x,y) | -Object(x). [resolve(6,b,7,b)]. given #9 (I,wt=5): 19 -Is_the(x,y) | -Object(y). [resolve(8,b,7,b)]. given #10 (I,wt=16): 20 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Ex1(z,u). [resolve(9,b,6,b)]. given #11 (I,wt=16): 21 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Is_the(u,z). [resolve(9,b,8,b)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 14. % Level of proof is 4. % Maximum clause weight is 16. % Given clauses 11. 2 (all x all F (Ex1(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 x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(F,y)))) # label(non_clause). [assumption]. 5 (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) # label(goal). [goal]. 6 -Ex1(x,y) | Relation1(x). [clausify(2)]. 8 -Is_the(x,y) | Relation1(y). [clausify(3)]. 9 -Object(x) | -Relation1(y) | -Object(z) | -Is_the(x,y) | z != x | Ex1(y,z). [clausify(4)]. 15 Object(c3). [deny(5)]. 16 Is_the(c3,c1). [deny(5)]. 17 -Ex1(c1,c3). [deny(5)]. 20 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Ex1(z,u). [resolve(9,b,6,b)]. 21 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,y) | -Is_the(u,z). [resolve(9,b,8,b)]. 32 -Ex1(c1,x). [ur(20,a,15,a,b,15,a,c,16,a,d,xx,e,17,a)]. 33 $F. [ur(21,a,15,a,b,15,a,c,16,a,d,xx,f,16,a),unit_del(a,32)]. ============================== end of proof ========================== % Redundant proof: 34 $F. [ur(21,a,15,a,b,15,a,c,16,a,d,xx,f,14,a),unit_del(a,32)]. % Redundant proof: 35 $F. [ur(21,a,13,a,b,13,a,c,14,a,d,xx,f,16,a),unit_del(a,32)]. % Redundant proof: 36 $F. [ur(21,a,13,a,b,13,a,c,14,a,d,xx,f,14,a),unit_del(a,32)]. % Disable descendants (x means already disabled): 17x 31x 32 given #12 (I,wt=2): 22 -Object(c1). [resolve(10,a,7,b)]. given #13 (A,wt=3): 23 -Ex1(c3,x). [resolve(18,b,15,a)]. given #14 (F,wt=3): 24 -Ex1(c2,x). [resolve(18,b,13,a)]. given #15 (F,wt=3): 27 -Is_the(x,c3). [resolve(19,b,15,a)]. given #16 (F,wt=3): 28 -Is_the(x,c2). [resolve(19,b,13,a)]. given #17 (F,wt=3): 37 -Is_the(c1,x). [resolve(22,a,12,b)]. given #18 (A,wt=6): 25 -Ex1(x,y) | -Is_the(x,z). [resolve(18,b,12,b)]. given #19 (F,wt=3): 38 -Ex1(x,c1). [resolve(22,a,11,b)]. given #20 (F,wt=6): 26 -Ex1(x,y) | -Ex1(z,x). [resolve(18,b,11,b)]. given #21 (F,wt=6): 29 -Is_the(x,y) | -Is_the(y,z). [resolve(19,b,12,b)]. given #22 (F,wt=6): 30 -Is_the(x,y) | -Ex1(z,y). [resolve(19,b,11,b)]. ============================== STATISTICS ============================ Given=22. Generated=72. Kept=24. proofs=1. Usable=21. Sos=0. Demods=0. Limbo=0, Disabled=20. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=44. Back_subsumed=2. 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=31. Nonunit_bsub_feature_tests=19. Megabytes=0.04. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= SEARCH FAILED Exiting with 1 proof. Process 13273 exit (sos_empty) Thu Oct 9 22:15:13 2008