============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 8112 was started by zalta on mally, Tue Jul 24 18:01:02 2007 The command was "prove". ============================== 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 F all x all w (Relation1(F) & Object(x) & Object(w) -> (Is_the(x,F) & x = w <-> (exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))) & y = w))))). end_of_list. formulas(goals). (all x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(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 (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 F all x all w (Relation1(F) & Object(x) & Object(w) -> (Is_the(x,F) & x = w <-> (exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))) & y = w))))) # label(non_clause). [assumption]. 5 (all x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(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)]. -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)]. -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | Object(f1(x,y,z)). [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | Ex1(x,f1(x,y,z)). [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | -Object(u) | -Ex1(x,u) | u = f1(x,y,z). [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | f1(x,y,z) = z. [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | Is_the(y,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | u != z. [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | Is_the(y,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | Is_the(y,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | z = y | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | u != z. [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | z = y | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. -Relation1(x) | -Object(y) | -Object(z) | z = y | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. Object(c1). [deny(5)]. Relation1(c2). [deny(5)]. Object(c3). [deny(5)]. Is_the(c1,c2). [deny(5)]. c3 = c1. [deny(5)]. -Ex1(c2,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 -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | Object(f1(x,y,z)). [clausify(4)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Object(f1(z,x,y)) | -Ex1(z,u). [resolve(9,a,6,b)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Object(f1(z,x,y)) | -Is_the(u,z). [resolve(9,a,8,b)]. 10 -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | Ex1(x,f1(x,y,z)). [clausify(4)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,f1(z,x,y)) | -Ex1(z,u). [resolve(10,a,6,b)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,f1(z,x,y)) | -Is_the(u,z). [resolve(10,a,8,b)]. 11 -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | -Object(u) | -Ex1(x,u) | u = f1(x,y,z). [clausify(4)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | -Object(u) | -Ex1(z,u) | u = f1(z,x,y) | -Ex1(z,w). [resolve(11,a,6,b)]. 12 -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | f1(x,y,z) = z. [clausify(4)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | f1(z,x,y) = y | -Ex1(z,u). [resolve(12,a,6,b)]. Derived: -Object(x) | -Object(y) | -Is_the(x,z) | y != x | f1(z,x,y) = y | -Is_the(u,z). [resolve(12,a,8,b)]. 13 -Relation1(x) | -Object(y) | -Object(z) | Is_the(y,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | Object(f2(z,x,y,u)) | u != y | -Ex1(z,w). [resolve(13,a,6,b)]. 14 -Relation1(x) | -Object(y) | -Object(z) | Is_the(y,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | Ex1(z,f2(z,x,y,u)) | u != y | -Ex1(z,w). [resolve(14,a,6,b)]. 15 -Relation1(x) | -Object(y) | -Object(z) | Is_the(y,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. Derived: -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | f2(z,x,y,u) != u | u != y | -Ex1(z,w). [resolve(15,a,6,b)]. 16 -Relation1(x) | -Object(y) | -Object(z) | z = y | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | Object(f2(u,x,y,z)) | z != y | -Ex1(u,w). [resolve(16,a,6,b)]. 17 -Relation1(x) | -Object(y) | -Object(z) | z = y | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | Ex1(u,f2(u,x,y,z)) | z != y | -Ex1(u,w). [resolve(17,a,6,b)]. 18 -Relation1(x) | -Object(y) | -Object(z) | z = y | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. Derived: -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | f2(u,x,y,z) != z | z != y | -Ex1(u,w). [resolve(18,a,6,b)]. 19 Relation1(c2). [deny(5)]. Derived: -Object(c2). [resolve(19,a,7,b)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Object, Ex1, Is_the ]). Function symbol precedence: function_order([ c1, c2, c3, 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). 20 -Ex1(x,y) | Object(y). [clausify(2)]. 21 -Is_the(x,y) | Object(x). [clausify(3)]. 22 Object(c1). [deny(5)]. 24 Is_the(c1,c2). [deny(5)]. 25 c3 = c1. [deny(5)]. 27 -Ex1(c2,c1). [copy(26),rewrite([25(2)])]. 28 -Ex1(x,y) | -Object(x). [resolve(6,b,7,b)]. 29 -Is_the(x,y) | -Object(y). [resolve(8,b,7,b)]. 44 -Object(c2). [resolve(19,a,7,b)]. 47 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Object(f1(z,x,y)). [factor(31,c,f)]. 50 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,f1(z,x,y)). [factor(33,c,f)]. 53 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | -Object(u) | -Ex1(z,u) | f1(z,x,y) = u. [factor(35,f,h)]. 56 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | f1(z,x,y) = y. [factor(37,c,f)]. 60 -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | Object(f2(z,x,y,u)) | u != y. [factor(38,e,h)]. 64 -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | Ex1(z,f2(z,x,y,u)) | u != y. [factor(39,e,h)]. 68 -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | f2(z,x,y,u) != u | u != y. [factor(40,e,h)]. 71 -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | Object(f2(u,x,y,z)) | z != y. [factor(41,e,h)]. 74 -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | Ex1(u,f2(u,x,y,z)) | z != y. [factor(42,e,h)]. 77 -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | f2(u,x,y,z) != z | z != y. [factor(43,e,h)]. 78 -Object(x) | -Is_the(x,y) | Object(f1(y,x,x)). [factor(46,b,d)]. 79 -Object(x) | -Is_the(x,y) | Ex1(y,f1(y,x,x)). [factor(49,b,d)]. 80 -Object(x) | -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,x,x) = z. [factor(51,d,f)]. 81 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | -Ex1(z,x) | f1(z,x,y) = x. [factor(52,e,g)]. 82 -Object(x) | -Is_the(x,y) | f1(y,x,x) = x. [factor(55,b,d)]. 84 -Object(x) | Is_the(x,y) | -Object(z) | -Ex1(y,z) | Object(f2(y,x,x,z)) | z != x. [factor(57,d,g)]. 85 -Object(x) | -Object(y) | Is_the(x,z) | -Ex1(z,x) | Object(f2(z,x,y,x)) | x != y. [factor(58,d,g)]. 86 -Object(x) | -Object(y) | Is_the(x,z) | -Ex1(z,y) | Object(f2(z,x,y,y)). [factor(59,d,f)]. 88 -Object(x) | Is_the(x,y) | -Object(z) | -Ex1(y,z) | Ex1(y,f2(y,x,x,z)) | z != x. [factor(61,d,g)]. 89 -Object(x) | -Object(y) | Is_the(x,z) | -Ex1(z,x) | Ex1(z,f2(z,x,y,x)) | x != y. [factor(62,d,g)]. 90 -Object(x) | -Object(y) | Is_the(x,z) | -Ex1(z,y) | Ex1(z,f2(z,x,y,y)). [factor(63,d,f)]. 92 -Object(x) | Is_the(x,y) | -Object(z) | -Ex1(y,z) | f2(y,x,x,z) != z | z != x. [factor(65,d,g)]. 93 -Object(x) | -Object(y) | Is_the(x,z) | -Ex1(z,x) | f2(z,x,y,x) != x | x != y. [factor(66,d,g)]. 94 -Object(x) | -Object(y) | Is_the(x,z) | -Ex1(z,y) | f2(z,x,y,y) != y. [factor(67,d,f)]. 95 -Object(x) | -Object(y) | y = x | -Ex1(z,x) | Object(f2(z,x,y,x)) | x != y. [factor(69,d,g)]. 96 -Object(x) | -Object(y) | y = x | -Ex1(z,y) | Object(f2(z,x,y,y)). [factor(70,d,f)]. 97 -Object(x) | -Object(y) | y = x | -Ex1(z,x) | Ex1(z,f2(z,x,y,x)) | x != y. [factor(72,d,g)]. 98 -Object(x) | -Object(y) | y = x | -Ex1(z,y) | Ex1(z,f2(z,x,y,y)). [factor(73,d,f)]. 99 -Object(x) | -Object(y) | y = x | -Ex1(z,x) | f2(z,x,y,x) != x | x != y. [factor(75,d,g)]. 100 -Object(x) | -Object(y) | y = x | -Ex1(z,y) | f2(z,x,y,y) != y. [factor(76,d,f)]. 101 -Object(x) | Is_the(x,y) | -Ex1(y,x) | Object(f2(y,x,x,x)). [factor(83,c,e)]. 102 -Object(x) | Is_the(x,y) | -Ex1(y,x) | Ex1(y,f2(y,x,x,x)). [factor(87,c,e)]. 103 -Object(x) | Is_the(x,y) | -Ex1(y,x) | f2(y,x,x,x) != x. [factor(91,c,e)]. end_of_list. formulas(demodulators). 25 c3 = c1. [deny(5)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=5): 20 -Ex1(x,y) | Object(y). [clausify(2)]. given #2 (I,wt=5): 21 -Is_the(x,y) | Object(x). [clausify(3)]. given #3 (I,wt=2): 22 Object(c1). [deny(5)]. given #4 (I,wt=3): 24 Is_the(c1,c2). [deny(5)]. given #5 (I,wt=3): 25 c3 = c1. [deny(5)]. given #6 (I,wt=3): 27 -Ex1(c2,c1). [copy(26),rewrite([25(2)])]. given #7 (I,wt=5): 28 -Ex1(x,y) | -Object(x). [resolve(6,b,7,b)]. given #8 (I,wt=5): 29 -Is_the(x,y) | -Object(y). [resolve(8,b,7,b)]. given #9 (I,wt=2): 44 -Object(c2). [resolve(19,a,7,b)]. given #10 (I,wt=15): 47 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Object(f1(z,x,y)). [factor(31,c,f)]. given #11 (I,wt=16): 50 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,f1(z,x,y)). [factor(33,c,f)]. given #12 (I,wt=21): 53 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | -Object(u) | -Ex1(z,u) | f1(z,x,y) = u. [factor(35,f,h)]. given #13 (I,wt=16): 56 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | f1(z,x,y) = y. [factor(37,c,f)]. given #14 (I,wt=21): 60 -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | Object(f2(z,x,y,u)) | u != y. [factor(38,e,h)]. given #15 (I,wt=22): 64 -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | Ex1(z,f2(z,x,y,u)) | u != y. [factor(39,e,h)]. given #16 (I,wt=22): 68 -Object(x) | -Object(y) | Is_the(x,z) | -Object(u) | -Ex1(z,u) | f2(z,x,y,u) != u | u != y. [factor(40,e,h)]. given #17 (I,wt=21): 71 -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | Object(f2(u,x,y,z)) | z != y. [factor(41,e,h)]. given #18 (I,wt=22): 74 -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | Ex1(u,f2(u,x,y,z)) | z != y. [factor(42,e,h)]. given #19 (I,wt=22): 77 -Object(x) | -Object(y) | y = x | -Object(z) | -Ex1(u,z) | f2(u,x,y,z) != z | z != y. [factor(43,e,h)]. given #20 (I,wt=10): 78 -Object(x) | -Is_the(x,y) | Object(f1(y,x,x)). [factor(46,b,d)]. given #21 (I,wt=11): 79 -Object(x) | -Is_the(x,y) | Ex1(y,f1(y,x,x)). [factor(49,b,d)]. given #22 (I,wt=16): 80 -Object(x) | -Is_the(x,y) | -Object(z) | -Ex1(y,z) | f1(y,x,x) = z. [factor(51,d,f)]. given #23 (I,wt=19): 81 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | -Ex1(z,x) | f1(z,x,y) = x. [factor(52,e,g)]. given #24 (I,wt=11): 82 -Object(x) | -Is_the(x,y) | f1(y,x,x) = x. [factor(55,b,d)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 20. % Level of proof is 6. % Maximum clause weight is 19. % Given clauses 24. 3 (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))) # label(non_clause). [assumption]. 4 (all F all x all w (Relation1(F) & Object(x) & Object(w) -> (Is_the(x,F) & x = w <-> (exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))) & y = w))))) # label(non_clause). [assumption]. 5 (all x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(F,y)))) # label(non_clause) # label(goal). [goal]. 8 -Is_the(x,y) | Relation1(y). [clausify(3)]. 10 -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | Ex1(x,f1(x,y,z)). [clausify(4)]. 12 -Relation1(x) | -Object(y) | -Object(z) | -Is_the(y,x) | z != y | f1(x,y,z) = z. [clausify(4)]. 22 Object(c1). [deny(5)]. 24 Is_the(c1,c2). [deny(5)]. 25 c3 = c1. [deny(5)]. 26 -Ex1(c2,c3). [deny(5)]. 27 -Ex1(c2,c1). [copy(26),rewrite([25(2)])]. 33 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | Ex1(z,f1(z,x,y)) | -Is_the(u,z). [resolve(10,a,8,b)]. 37 -Object(x) | -Object(y) | -Is_the(x,z) | y != x | f1(z,x,y) = y | -Is_the(u,z). [resolve(12,a,8,b)]. 49 -Object(x) | -Is_the(x,y) | Ex1(y,f1(y,x,x)) | -Is_the(z,y). [factor(33,a,b),xx(c)]. 55 -Object(x) | -Is_the(x,y) | f1(y,x,x) = x | -Is_the(z,y). [factor(37,a,b),xx(c)]. 79 -Object(x) | -Is_the(x,y) | Ex1(y,f1(y,x,x)). [factor(49,b,d)]. 82 -Object(x) | -Is_the(x,y) | f1(y,x,x) = x. [factor(55,b,d)]. 114 Ex1(c2,f1(c2,c1,c1)). [resolve(79,b,24,a),unit_del(a,22)]. 116 f1(c2,c1,c1) = c1. [resolve(82,b,24,a),unit_del(a,22)]. 118 $F. [back_rewrite(114),rewrite([116(5)]),unit_del(a,27)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=24. Generated=162. Kept=96. proofs=1. Usable=24. Sos=27. Demods=2. Limbo=2, Disabled=80. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=65. Back_subsumed=40. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2 (0 lex), Back_demodulated=3. Back_unit_deleted=0. Demod_attempts=1146. Demod_rewrites=4. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=244. Nonunit_bsub_feature_tests=260. Megabytes=0.11. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 8112 exit (max_proofs) Tue Jul 24 18:01:02 2007