============================== 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 (exemplifies1(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) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(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 -> 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 all w (relation1(F) & object(x) & object(w) -> (is_the(x,F) & x = w <-> (exists y (object(y) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(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 -> 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) | -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 | exemplifies1(x,f1(x,y,z)). [clausify(4)]. -relation1(x) | -object(y) | -object(z) | -is_the(y,x) | z != y | -object(u) | -exemplifies1(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) | -exemplifies1(x,u) | object(f2(x,y,z,u)) | u != z. [clausify(4)]. -relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | exemplifies1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. -relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. -relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | object(f2(x,y,z,u)) | u != z. [clausify(4)]. -relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | exemplifies1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. -relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(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)]. -exemplifies1(c2,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) | -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)) | -exemplifies1(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 | exemplifies1(x,f1(x,y,z)). [clausify(4)]. Derived: -object(x) | -object(y) | -is_the(x,z) | y != x | exemplifies1(z,f1(z,x,y)) | -exemplifies1(z,u). [resolve(10,a,6,b)]. Derived: -object(x) | -object(y) | -is_the(x,z) | y != x | exemplifies1(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) | -exemplifies1(x,u) | u = f1(x,y,z). [clausify(4)]. Derived: -object(x) | -object(y) | -is_the(x,z) | y != x | -object(u) | -exemplifies1(z,u) | u = f1(z,x,y) | -exemplifies1(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 | -exemplifies1(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) | -exemplifies1(x,u) | object(f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -object(x) | -object(y) | is_the(x,z) | -object(u) | -exemplifies1(z,u) | object(f2(z,x,y,u)) | u != y | -exemplifies1(z,w). [resolve(13,a,6,b)]. 14 -relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | exemplifies1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -object(x) | -object(y) | is_the(x,z) | -object(u) | -exemplifies1(z,u) | exemplifies1(z,f2(z,x,y,u)) | u != y | -exemplifies1(z,w). [resolve(14,a,6,b)]. 15 -relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. Derived: -object(x) | -object(y) | is_the(x,z) | -object(u) | -exemplifies1(z,u) | f2(z,x,y,u) != u | u != y | -exemplifies1(z,w). [resolve(15,a,6,b)]. 16 -relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | object(f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -object(x) | -object(y) | y = x | -object(z) | -exemplifies1(u,z) | object(f2(u,x,y,z)) | z != y | -exemplifies1(u,w). [resolve(16,a,6,b)]. 17 -relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | exemplifies1(x,f2(x,y,z,u)) | u != z. [clausify(4)]. Derived: -object(x) | -object(y) | y = x | -object(z) | -exemplifies1(u,z) | exemplifies1(u,f2(u,x,y,z)) | z != y | -exemplifies1(u,w). [resolve(17,a,6,b)]. 18 -relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | f2(x,y,z,u) != u | u != z. [clausify(4)]. Derived: -object(x) | -object(y) | y = x | -object(z) | -exemplifies1(u,z) | f2(u,x,y,z) != z | z != y | -exemplifies1(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, exemplifies1, 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 -exemplifies1(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 -exemplifies1(c2,c1). [copy(26),rewrite([25(2)])]. 28 -exemplifies1(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 | exemplifies1(z,f1(z,x,y)). [factor(33,c,f)]. 53 -object(x) | -object(y) | -is_the(x,z) | y != x | -object(u) | -exemplifies1(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) | -exemplifies1(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) | -exemplifies1(z,u) | exemplifies1(z,f2(z,x,y,u)) | u != y. [factor(39,e,h)]. 68 -object(x) | -object(y) | is_the(x,z) | -object(u) | -exemplifies1(z,u) | f2(z,x,y,u) != u | u != y. [factor(40,e,h)]. 71 -object(x) | -object(y) | y = x | -object(z) | -exemplifies1(u,z) | object(f2(u,x,y,z)) | z != y. [factor(41,e,h)]. 74 -object(x) | -object(y) | y = x | -object(z) | -exemplifies1(u,z) | exemplifies1(u,f2(u,x,y,z)) | z != y. [factor(42,e,h)]. 77 -object(x) | -object(y) | y = x | -object(z) | -exemplifies1(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) | exemplifies1(y,f1(y,x,x)). [factor(49,b,d)]. 80 -object(x) | -is_the(x,y) | -object(z) | -exemplifies1(y,z) | f1(y,x,x) = z. [factor(51,d,f)]. 81 -object(x) | -object(y) | -is_the(x,z) | y != x | -exemplifies1(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) | -exemplifies1(y,z) | object(f2(y,x,x,z)) | z != x. [factor(57,d,g)]. 85 -object(x) | -object(y) | is_the(x,z) | -exemplifies1(z,x) | object(f2(z,x,y,x)) | x != y. [factor(58,d,g)]. 86 -object(x) | -object(y) | is_the(x,z) | -exemplifies1(z,y) | object(f2(z,x,y,y)). [factor(59,d,f)]. 88 -object(x) | is_the(x,y) | -object(z) | -exemplifies1(y,z) | exemplifies1(y,f2(y,x,x,z)) | z != x. [factor(61,d,g)]. 89 -object(x) | -object(y) | is_the(x,z) | -exemplifies1(z,x) | exemplifies1(z,f2(z,x,y,x)) | x != y. [factor(62,d,g)]. 90 -object(x) | -object(y) | is_the(x,z) | -exemplifies1(z,y) | exemplifies1(z,f2(z,x,y,y)). [factor(63,d,f)]. 92 -object(x) | is_the(x,y) | -object(z) | -exemplifies1(y,z) | f2(y,x,x,z) != z | z != x. [factor(65,d,g)]. 93 -object(x) | -object(y) | is_the(x,z) | -exemplifies1(z,x) | f2(z,x,y,x) != x | x != y. [factor(66,d,g)]. 94 -object(x) | -object(y) | is_the(x,z) | -exemplifies1(z,y) | f2(z,x,y,y) != y. [factor(67,d,f)]. 95 -object(x) | -object(y) | y = x | -exemplifies1(z,x) | object(f2(z,x,y,x)) | x != y. [factor(69,d,g)]. 96 -object(x) | -object(y) | y = x | -exemplifies1(z,y) | object(f2(z,x,y,y)). [factor(70,d,f)]. 97 -object(x) | -object(y) | y = x | -exemplifies1(z,x) | exemplifies1(z,f2(z,x,y,x)) | x != y. [factor(72,d,g)]. 98 -object(x) | -object(y) | y = x | -exemplifies1(z,y) | exemplifies1(z,f2(z,x,y,y)). [factor(73,d,f)]. 99 -object(x) | -object(y) | y = x | -exemplifies1(z,x) | f2(z,x,y,x) != x | x != y. [factor(75,d,g)]. 100 -object(x) | -object(y) | y = x | -exemplifies1(z,y) | f2(z,x,y,y) != y. [factor(76,d,f)]. 101 -object(x) | is_the(x,y) | -exemplifies1(y,x) | object(f2(y,x,x,x)). [factor(83,c,e)]. 102 -object(x) | is_the(x,y) | -exemplifies1(y,x) | exemplifies1(y,f2(y,x,x,x)). [factor(87,c,e)]. 103 -object(x) | is_the(x,y) | -exemplifies1(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 -exemplifies1(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 -exemplifies1(c2,c1). [copy(26),rewrite([25(2)])]. given #7 (I,wt=5): 28 -exemplifies1(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 | exemplifies1(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) | -exemplifies1(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) | -exemplifies1(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) | -exemplifies1(z,u) | exemplifies1(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) | -exemplifies1(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) | -exemplifies1(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) | -exemplifies1(u,z) | exemplifies1(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) | -exemplifies1(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) | exemplifies1(y,f1(y,x,x)). [factor(49,b,d)]. given #22 (I,wt=16): 80 -object(x) | -is_the(x,y) | -object(z) | -exemplifies1(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 | -exemplifies1(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) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(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 -> exemplifies1(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 | exemplifies1(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 -exemplifies1(c2,c3). [deny(5)]. 27 -exemplifies1(c2,c1). [copy(26),rewrite([25(2)])]. 33 -object(x) | -object(y) | -is_the(x,z) | y != x | exemplifies1(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) | exemplifies1(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) | exemplifies1(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 exemplifies1(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