============================== Prover9 =============================== Prover9 (32) version June-2007, June 2007. Process 13272 was started by zalta on mally, Thu Oct 9 22:15:08 2008 The command was "prover9". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all F all G all x (Relation1(F) & Relation1(G) & Object(x) -> (Is_the(x,F) & Ex1(G,x) <-> (exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))) & Ex1(G,y)))))). end_of_list. formulas(goals). (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)))))). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all F all G all x (Relation1(F) & Relation1(G) & Object(x) -> (Is_the(x,F) & Ex1(G,x) <-> (exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))) & Ex1(G,y)))))) # label(non_clause). [assumption]. 2 (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) # 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) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Object(f1(x,y,z)). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Ex1(x,f1(x,y,z)). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | -Object(u) | -Ex1(x,u) | u = f1(x,y,z). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Ex1(y,f1(x,y,z)). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. Relation1(c1). [deny(2)]. Object(c2). [deny(2)]. Ex1(c1,c2). [deny(2)]. -Object(x) | -Ex1(c1,x) | x = c2. [deny(2)]. -Object(x) | -Is_the(x,c1). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Object, Relation1, Ex1, Is_the ]). Function symbol precedence: function_order([ c1, c2, 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). 3 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Object(f1(x,y,z)). [clausify(1)]. 4 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Ex1(x,f1(x,y,z)). [clausify(1)]. 6 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | -Object(u) | -Ex1(x,u) | f1(x,y,z) = u. [copy(5),flip(h)]. 7 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Ex1(y,f1(x,y,z)). [clausify(1)]. 8 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. 9 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. 10 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. 11 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. 12 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. 13 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. 14 Relation1(c1). [deny(2)]. 15 Object(c2). [deny(2)]. 16 Ex1(c1,c2). [deny(2)]. 18 -Object(x) | -Ex1(c1,x) | c2 = x. [copy(17),flip(c)]. 19 -Object(x) | -Is_the(x,c1). [deny(2)]. 20 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | Object(f1(x,x,y)). [factor(3,a,b)]. 21 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | Ex1(x,f1(x,x,y)). [factor(4,a,b)]. 22 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | -Object(z) | -Ex1(x,z) | f1(x,x,y) = z. [factor(6,a,b)]. 23 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | -Ex1(x,z) | f1(x,y,z) = z. [factor(6,c,f)]. 24 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | f1(x,x,y) = y. [factor(6,e,g),merge(b),merge(f)]. 25 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | Object(f2(x,x,y,z)). [factor(8,a,b),merge(g)]. 26 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Ex1(x,z) | Object(f2(x,y,z,z)) | -Ex1(y,z). [factor(8,c,e)]. 27 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | Ex1(x,f2(x,x,y,z)). [factor(9,a,b),merge(g)]. 28 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Ex1(x,z) | Ex1(x,f2(x,y,z,z)) | -Ex1(y,z). [factor(9,c,e)]. 29 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | f2(x,x,y,z) != z. [factor(10,a,b),merge(g)]. 30 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Ex1(x,z) | f2(x,y,z,z) != z | -Ex1(y,z). [factor(10,c,e)]. 31 -Relation1(x) | -Object(y) | Ex1(x,y) | -Object(z) | -Ex1(x,z) | Object(f2(x,x,y,z)). [factor(11,a,b),merge(g)]. 32 -Relation1(x) | -Object(y) | Ex1(x,y) | -Object(z) | -Ex1(x,z) | Ex1(x,f2(x,x,y,z)). [factor(12,a,b),merge(g)]. 33 -Relation1(x) | -Object(y) | Ex1(x,y) | -Object(z) | -Ex1(x,z) | f2(x,x,y,z) != z. [factor(13,a,b),merge(g)]. 34 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | Object(f2(x,x,y,y)). [factor(25,b,d)]. 35 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | Ex1(x,f2(x,x,y,y)). [factor(27,b,d)]. 36 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | f2(x,x,y,y) != y. [factor(29,b,d)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=17): 3 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Object(f1(x,y,z)). [clausify(1)]. given #2 (I,wt=18): 4 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Ex1(x,f1(x,y,z)). [clausify(1)]. given #3 (I,wt=23): 6 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | -Object(u) | -Ex1(x,u) | f1(x,y,z) = u. [copy(5),flip(h)]. given #4 (I,wt=18): 7 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | Ex1(y,f1(x,y,z)). [clausify(1)]. given #5 (I,wt=23): 8 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. given #6 (I,wt=24): 9 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. given #7 (I,wt=24): 10 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. given #8 (I,wt=23): 11 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. given #9 (I,wt=24): 12 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. given #10 (I,wt=24): 13 -Relation1(x) | -Relation1(y) | -Object(z) | Ex1(y,z) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. given #11 (I,wt=2): 14 Relation1(c1). [deny(2)]. given #12 (I,wt=2): 15 Object(c2). [deny(2)]. given #13 (I,wt=3): 16 Ex1(c1,c2). [deny(2)]. given #14 (I,wt=8): 18 -Object(x) | -Ex1(c1,x) | c2 = x. [copy(17),flip(c)]. given #15 (I,wt=5): 19 -Object(x) | -Is_the(x,c1). [deny(2)]. given #16 (I,wt=15): 20 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | Object(f1(x,x,y)). [factor(3,a,b)]. given #17 (I,wt=16): 21 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | Ex1(x,f1(x,x,y)). [factor(4,a,b)]. given #18 (I,wt=21): 22 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | -Object(z) | -Ex1(x,z) | f1(x,x,y) = z. [factor(6,a,b)]. given #19 (I,wt=21): 23 -Relation1(x) | -Relation1(y) | -Object(z) | -Is_the(z,x) | -Ex1(y,z) | -Ex1(x,z) | f1(x,y,z) = z. [factor(6,c,f)]. given #20 (I,wt=16): 24 -Relation1(x) | -Object(y) | -Is_the(y,x) | -Ex1(x,y) | f1(x,x,y) = y. [factor(6,e,g),merge(b),merge(f)]. given #21 (I,wt=18): 25 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | Object(f2(x,x,y,z)). [factor(8,a,b),merge(g)]. given #22 (I,wt=21): 26 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Ex1(x,z) | Object(f2(x,y,z,z)) | -Ex1(y,z). [factor(8,c,e)]. given #23 (I,wt=19): 27 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | Ex1(x,f2(x,x,y,z)). [factor(9,a,b),merge(g)]. given #24 (I,wt=22): 28 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Ex1(x,z) | Ex1(x,f2(x,y,z,z)) | -Ex1(y,z). [factor(9,c,e)]. given #25 (I,wt=19): 29 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | f2(x,x,y,z) != z. [factor(10,a,b),merge(g)]. given #26 (I,wt=22): 30 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Ex1(x,z) | f2(x,y,z,z) != z | -Ex1(y,z). [factor(10,c,e)]. given #27 (I,wt=18): 31 -Relation1(x) | -Object(y) | Ex1(x,y) | -Object(z) | -Ex1(x,z) | Object(f2(x,x,y,z)). [factor(11,a,b),merge(g)]. given #28 (I,wt=19): 32 -Relation1(x) | -Object(y) | Ex1(x,y) | -Object(z) | -Ex1(x,z) | Ex1(x,f2(x,x,y,z)). [factor(12,a,b),merge(g)]. given #29 (I,wt=19): 33 -Relation1(x) | -Object(y) | Ex1(x,y) | -Object(z) | -Ex1(x,z) | f2(x,x,y,z) != z. [factor(13,a,b),merge(g)]. given #30 (I,wt=16): 34 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | Object(f2(x,x,y,y)). [factor(25,b,d)]. given #31 (I,wt=17): 35 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | Ex1(x,f2(x,x,y,y)). [factor(27,b,d)]. given #32 (I,wt=17): 36 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | f2(x,x,y,y) != y. [factor(29,b,d)]. given #33 (A,wt=17): 37 -Relation1(x) | -Object(y) | Ex1(c1,y) | -Ex1(x,c2) | f2(x,c1,y,c2) != c2. [resolve(16,a,13,h),unit_del(b,14),unit_del(e,15)]. given #34 (F,wt=3): 49 -Is_the(c2,c1). [ur(19,a,15,a)]. given #35 (F,wt=7): 64 f2(c1,c1,c2,c2) != c2. [resolve(36,d,16,a),unit_del(a,14),unit_del(b,15),unit_del(c,49)]. given #36 (F,wt=12): 57 -Relation1(x) | f2(c1,x,c2,c2) != c2 | -Ex1(x,c2). [resolve(30,e,16,a),unit_del(a,14),unit_del(c,15),unit_del(d,49)]. given #37 (T,wt=6): 62 Object(f2(c1,c1,c2,c2)). [resolve(34,d,16,a),unit_del(a,14),unit_del(b,15),unit_del(c,49)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 22. % Level of proof is 5. % Maximum clause weight is 24. % Given clauses 37. 1 (all F all G all x (Relation1(F) & Relation1(G) & Object(x) -> (Is_the(x,F) & Ex1(G,x) <-> (exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))) & Ex1(G,y)))))) # label(non_clause). [assumption]. 2 (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) # label(goal). [goal]. 8 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Object(f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. 9 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | Ex1(x,f2(x,y,z,u)) | -Ex1(y,u). [clausify(1)]. 10 -Relation1(x) | -Relation1(y) | -Object(z) | Is_the(z,x) | -Object(u) | -Ex1(x,u) | f2(x,y,z,u) != u | -Ex1(y,u). [clausify(1)]. 14 Relation1(c1). [deny(2)]. 15 Object(c2). [deny(2)]. 16 Ex1(c1,c2). [deny(2)]. 17 -Object(x) | -Ex1(c1,x) | x = c2. [deny(2)]. 18 -Object(x) | -Ex1(c1,x) | c2 = x. [copy(17),flip(c)]. 19 -Object(x) | -Is_the(x,c1). [deny(2)]. 25 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | Object(f2(x,x,y,z)). [factor(8,a,b),merge(g)]. 27 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | Ex1(x,f2(x,x,y,z)). [factor(9,a,b),merge(g)]. 29 -Relation1(x) | -Object(y) | Is_the(y,x) | -Object(z) | -Ex1(x,z) | f2(x,x,y,z) != z. [factor(10,a,b),merge(g)]. 34 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | Object(f2(x,x,y,y)). [factor(25,b,d)]. 35 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | Ex1(x,f2(x,x,y,y)). [factor(27,b,d)]. 36 -Relation1(x) | -Object(y) | Is_the(y,x) | -Ex1(x,y) | f2(x,x,y,y) != y. [factor(29,b,d)]. 49 -Is_the(c2,c1). [ur(19,a,15,a)]. 62 Object(f2(c1,c1,c2,c2)). [resolve(34,d,16,a),unit_del(a,14),unit_del(b,15),unit_del(c,49)]. 63 Ex1(c1,f2(c1,c1,c2,c2)). [resolve(35,d,16,a),unit_del(a,14),unit_del(b,15),unit_del(c,49)]. 64 f2(c1,c1,c2,c2) != c2. [resolve(36,d,16,a),unit_del(a,14),unit_del(b,15),unit_del(c,49)]. 66 $F. [ur(18,a,62,a,c,64,a(flip)),unit_del(a,63)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=37. Generated=93. Kept=61. proofs=1. Usable=37. Sos=23. Demods=0. Limbo=1, Disabled=15. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=31. Back_subsumed=0. 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=90. Megabytes=0.09. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13272 exit (max_proofs) Thu Oct 9 22:15:08 2008