============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3738 was started by zalta on mally, Wed Jun 14 17:08:22 2006 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= op(300,prefix,~). set(auto2). % set(auto2) -> set(auto). % set(auto) -> set(auto_inference). % set(auto_inference) -> set(predicate_elim). % set(auto_inference) -> assign(eq_defs, unfold). % set(auto) -> set(auto_limits). % set(auto_limits) -> assign(max_weight, 100). % set(auto_limits) -> assign(sos_limit, 10000). % set(auto2) -> set(fof_reduction). % set(auto2) -> assign(new_constants, 1). % set(auto2) -> assign(fold_denial_max, 3). % set(auto2) -> assign(max_weight, 200). % set(auto2) -> assign(nest_penalty, 1). % set(auto2) -> assign(skolem_penalty, 3). % set(auto2) -> assign(sk_constant_weight, 0). % set(auto2) -> assign(prop_atom_weight, 5). % set(auto2) -> set(sort_initial_sos). % set(auto2) -> assign(sos_limit, -1). % set(auto2) -> assign(lrs_ticks, 3000). % set(auto2) -> assign(max_megs, 400). % set(auto2) -> assign(stats, some). % set(auto2) -> clear(echo_input). % set(auto2) -> set(quiet). % set(auto2) -> clear(print_subproblems). % set(auto2) -> clear(print_initial_clauses). % set(auto2) -> clear(print_given). clear(fof_reduction). set(print_initial_clauses). % formulas(sos). % not echoed (7 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 Object(c1). [clausify]. 2 Ex1At(A,c1,W). [clausify]. 3 - Situation(x) | - Maximal1(x). [clausify]. 4 - Proposition(x) | Property(VAC(x)). [clausify]. 5 - Object(x) | - Maximal1(x) | Situation(x). [clausify]. 6 - Object(x) | - Situation(x) | Ex1At(A,x,W). [clausify]. 7 - Property(x) | - Enc(c1,x) | Proposition(f5(x)). [clausify]. 8 - Object(x) | Maximal1(x) | - Situation(x) | Proposition(f4(x)). [clausify]. 9 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 10 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 11 - Object(x) | Maximal1(x) | - Situation(x) | - TrueIn(f4(x),x). [clausify]. 12 - Property(x) | - Enc(c1,x) | VAC(f5(x)) = x. [clausify]. 13 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f1(x,y)). [clausify]. 14 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Property(f3(x)). [clausify]. 15 - Object(x) | Maximal1(x) | - Situation(x) | - TrueIn(~ f4(x),x). [clausify]. 16 - Property(x) | Enc(c1,x) | - Proposition(y) | VAC(y) != x. [clausify]. 17 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 18 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Enc(x,f3(x)). [clausify]. 19 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f1(x,y). [clausify]. 20 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)). [clausify]. 21 - Object(x) | - Maximal1(x) | - Proposition(y) | TrueIn(y,x) | TrueIn(~ y,x). [clausify]. 22 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y. [clausify]. 23 - Object(x) | Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | VAC(y) != f3(x). [clausify]. 24 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. end_of_list. clauses(demodulators). end_of_list. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 69 Ex1At(A,c1,W). [clausify]. 70 - Situation(x) | - Maximal1(x). [clausify]. 71 - Property(x) | - Enc(c1,x) | VAC(f5(x)) = x. [clausify]. 72 - Maximal1(c1) | Situation(c1). [resolve(5,a,1,a)]. 73 Maximal1(c1) | - Situation(c1) | - TrueIn(f4(c1),c1). [resolve(11,a,1,a)]. 74 Situation(c1) | Property(f3(c1)). [copy(32),unit_del(b,69)]. 75 Maximal1(c1) | - Situation(c1) | - TrueIn(~ f4(c1),c1). [resolve(15,a,1,a)]. 76 Situation(c1) | Enc(c1,f3(c1)). [copy(35),unit_del(b,69)]. 77 - Situation(c1) | - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [resolve(22,a,1,a)]. 78 - Property(x) | - Enc(c1,x) | Property(VAC(f5(x))). [resolve(7,c,4,a)]. 79 - Property(x) | Enc(c1,x) | VAC(f5(y)) != x | - Property(y) | - Enc(c1,y). [resolve(16,c,7,c)]. 80 Maximal1(c1) | - Situation(c1) | Property(VAC(f4(c1))). [resolve(27,c,4,a)]. 81 Maximal1(c1) | - Situation(c1) | - Property(x) | Enc(c1,x) | VAC(f4(c1)) != x. [resolve(27,c,16,c)]. 82 - TrueIn(f5(x),c1) | Encp(c1,f5(x)) | - Property(x) | - Enc(c1,x). [resolve(28,a,7,c)]. 83 TrueIn(f5(x),c1) | - Encp(c1,f5(x)) | - Property(x) | - Enc(c1,x). [resolve(29,a,7,c)]. 84 TrueIn(f4(c1),c1) | - Encp(c1,f4(c1)) | Maximal1(c1) | - Situation(c1). [resolve(29,a,27,c)]. 85 - Encp(c1,f5(x)) | Property(f1(c1,f5(x))) | - Property(x) | - Enc(c1,x). [resolve(31,a,7,c)]. 86 - Encp(c1,f4(c1)) | Property(f1(c1,f4(c1))) | Maximal1(c1) | - Situation(c1). [resolve(31,a,27,c)]. 87 - Encp(c1,f5(x)) | Enc(c1,f1(c1,f5(x))) | - Property(x) | - Enc(c1,x). [resolve(34,a,7,c)]. 88 - Encp(c1,f4(c1)) | Enc(c1,f1(c1,f4(c1))) | Maximal1(c1) | - Situation(c1). [resolve(34,a,27,c)]. 89 - Encp(c1,f5(x)) | VAC(f5(x)) = f1(c1,f5(x)) | - Property(x) | - Enc(c1,x). [resolve(36,a,7,c)]. 90 - Encp(c1,f4(c1)) | VAC(f4(c1)) = f1(c1,f4(c1)) | Maximal1(c1) | - Situation(c1). [resolve(36,a,27,c)]. 91 - Situation(c1) | - Property(x) | - Enc(c1,x) | Property(VAC(f2(c1,x))). [resolve(37,d,4,a)]. 92 - Situation(c1) | - Property(x) | - Enc(c1,x) | - Property(y) | Enc(c1,y) | VAC(f2(c1,x)) != y. [resolve(37,d,16,c)]. 93 - Situation(c1) | - Property(x) | - Enc(c1,x) | - TrueIn(f2(c1,x),c1) | Encp(c1,f2(c1,x)). [resolve(37,d,28,a)]. 94 - Situation(c1) | - Property(x) | - Enc(c1,x) | TrueIn(f2(c1,x),c1) | - Encp(c1,f2(c1,x)). [resolve(37,d,29,a)]. 95 - Situation(c1) | - Property(x) | - Enc(c1,x) | - Encp(c1,f2(c1,x)) | Property(f1(c1,f2(c1,x))). [resolve(37,d,31,a)]. 96 - Situation(c1) | - Property(x) | - Enc(c1,x) | - Encp(c1,f2(c1,x)) | Enc(c1,f1(c1,f2(c1,x))). [resolve(37,d,34,a)]. 97 - Situation(c1) | - Property(x) | - Enc(c1,x) | - Encp(c1,f2(c1,x)) | VAC(f2(c1,x)) = f1(c1,f2(c1,x)). [resolve(37,d,36,a)]. 98 - Maximal1(c1) | TrueIn(f5(x),c1) | TrueIn(~ f5(x),c1) | - Property(x) | - Enc(c1,x). [resolve(38,b,7,c)]. 99 Situation(c1) | VAC(f5(x)) != f3(c1) | - Property(x) | - Enc(c1,x). [copy(65),unit_del(b,69)]. 100 Encp(c1,f5(x)) | - Property(y) | VAC(f5(x)) != y | - Enc(c1,y) | - Property(x) | - Enc(c1,x). [resolve(41,a,7,c)]. 101 Encp(c1,f4(c1)) | - Property(x) | VAC(f4(c1)) != x | - Enc(c1,x) | Maximal1(c1) | - Situation(c1). [resolve(41,a,27,c)]. 102 Encp(c1,f2(c1,x)) | - Property(y) | VAC(f2(c1,x)) != y | - Enc(c1,y) | - Situation(c1) | - Property(x) | - Enc(c1,x). [resolve(41,a,37,d)]. 103 Encp(c1,f5(x)) | - Property(x) | VAC(f5(x)) != x | - Enc(c1,x). [factor(100,b,e),merge(e)]. 104 Encp(c1,f2(c1,x)) | - Property(x) | VAC(f2(c1,x)) != x | - Enc(c1,x) | - Situation(c1). [factor(102,b,f),merge(f)]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.01) seconds. % Length of proof is 60. % Level of proof is 22. % Maximum clause weight is 12. % Given clauses 61. 1 Object(c1). [clausify]. 4 - Proposition(x) | Property(VAC(x)). [clausify]. 7 - Property(x) | - Enc(c1,x) | Proposition(f5(x)). [clausify]. 8 - Object(x) | Maximal1(x) | - Situation(x) | Proposition(f4(x)). [clausify]. 10 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 11 - Object(x) | Maximal1(x) | - Situation(x) | - TrueIn(f4(x),x). [clausify]. 14 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Property(f3(x)). [clausify]. 16 - Property(x) | Enc(c1,x) | - Proposition(y) | VAC(y) != x. [clausify]. 18 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Enc(x,f3(x)). [clausify]. 23 - Object(x) | Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | VAC(y) != f3(x). [clausify]. 24 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 27 Maximal1(c1) | - Situation(c1) | Proposition(f4(c1)). [resolve(8,a,1,a)]. 29 - Proposition(x) | TrueIn(x,c1) | - Encp(c1,x). [resolve(10,a,1,a)]. 32 Situation(c1) | - Ex1At(A,c1,W) | Property(f3(c1)). [resolve(14,a,1,a)]. 35 Situation(c1) | - Ex1At(A,c1,W) | Enc(c1,f3(c1)). [resolve(18,a,1,a)]. 40 Situation(c1) | - Ex1At(A,c1,W) | - Proposition(x) | VAC(x) != f3(c1). [resolve(23,a,1,a)]. 41 - Proposition(x) | Encp(c1,x) | - Property(y) | VAC(x) != y | - Enc(c1,y). [resolve(24,a,1,a)]. 65 Situation(c1) | - Ex1At(A,c1,W) | VAC(f5(x)) != f3(c1) | - Property(x) | - Enc(c1,x). [resolve(40,c,7,c)]. 69 Ex1At(A,c1,W). [clausify]. 70 - Situation(x) | - Maximal1(x). [clausify]. 71 - Property(x) | - Enc(c1,x) | VAC(f5(x)) = x. [clausify]. 73 Maximal1(c1) | - Situation(c1) | - TrueIn(f4(c1),c1). [resolve(11,a,1,a)]. 74 Situation(c1) | Property(f3(c1)). [copy(32),unit_del(b,69)]. 76 Situation(c1) | Enc(c1,f3(c1)). [copy(35),unit_del(b,69)]. 80 Maximal1(c1) | - Situation(c1) | Property(VAC(f4(c1))). [resolve(27,c,4,a)]. 81 Maximal1(c1) | - Situation(c1) | - Property(x) | Enc(c1,x) | VAC(f4(c1)) != x. [resolve(27,c,16,c)]. 84 TrueIn(f4(c1),c1) | - Encp(c1,f4(c1)) | Maximal1(c1) | - Situation(c1). [resolve(29,a,27,c)]. 99 Situation(c1) | VAC(f5(x)) != f3(c1) | - Property(x) | - Enc(c1,x). [copy(65),unit_del(b,69)]. 101 Encp(c1,f4(c1)) | - Property(x) | VAC(f4(c1)) != x | - Enc(c1,x) | Maximal1(c1) | - Situation(c1). [resolve(41,a,27,c)]. 105 Situation(c1) | - Property(f3(c1)) | VAC(f5(f3(c1))) = f3(c1). [resolve(76,b,71,b)]. 108 Maximal1(c1) | Property(VAC(f4(c1))) | Property(f3(c1)). [resolve(80,b,74,a)]. 109 Maximal1(c1) | - Situation(c1) | - Property(VAC(f4(c1))) | Enc(c1,VAC(f4(c1))). [xx_res(81,e)]. 112 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | - Enc(c1,VAC(f4(c1))) | Maximal1(c1) | - Situation(c1). [xx_res(101,c)]. 114 Property(VAC(f4(c1))) | Property(f3(c1)) | - Situation(c1). [resolve(108,a,70,b)]. 115 Property(VAC(f4(c1))) | Property(f3(c1)). [resolve(114,c,74,a),merge(c)]. 116 Maximal1(c1) | - Property(VAC(f4(c1))) | Enc(c1,VAC(f4(c1))) | Property(f3(c1)). [resolve(109,b,74,a)]. 117 Maximal1(c1) | Enc(c1,VAC(f4(c1))) | Property(f3(c1)). [resolve(116,b,115,a),merge(d)]. 122 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | Maximal1(c1) | - Situation(c1) | Property(f3(c1)). [resolve(112,c,117,b),merge(e)]. 125 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | Maximal1(c1) | Property(f3(c1)). [resolve(122,d,74,a),merge(e)]. 126 Encp(c1,f4(c1)) | Maximal1(c1) | Property(f3(c1)). [resolve(125,b,115,a),merge(d)]. 130 Maximal1(c1) | Property(f3(c1)) | TrueIn(f4(c1),c1) | - Situation(c1). [resolve(126,a,84,b),merge(d)]. 131 Maximal1(c1) | Property(f3(c1)) | TrueIn(f4(c1),c1). [resolve(130,d,74,a),merge(d)]. 133 Maximal1(c1) | Property(f3(c1)) | - Situation(c1). [resolve(131,c,73,c),merge(c)]. 134 Maximal1(c1) | Property(f3(c1)). [resolve(133,c,74,a),merge(c)]. 135 Property(f3(c1)) | - Situation(c1). [resolve(134,a,70,b)]. 136 Property(f3(c1)). [resolve(135,b,74,a),merge(b)]. 139 Situation(c1) | VAC(f5(f3(c1))) = f3(c1). [back_unit_del(105),unit_del(b,136)]. 143 Situation(c1) | - Enc(c1,f3(c1)). [resolve(139,b,99,b),merge(b),unit_del(b,136)]. 144 Situation(c1). [resolve(143,b,76,b),merge(b)]. 146 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | - Enc(c1,VAC(f4(c1))) | Maximal1(c1). [back_unit_del(112),unit_del(e,144)]. 148 Maximal1(c1) | - Property(VAC(f4(c1))) | Enc(c1,VAC(f4(c1))). [back_unit_del(109),unit_del(b,144)]. 162 TrueIn(f4(c1),c1) | - Encp(c1,f4(c1)) | Maximal1(c1). [back_unit_del(84),unit_del(d,144)]. 164 Maximal1(c1) | Property(VAC(f4(c1))). [back_unit_del(80),unit_del(b,144)]. 167 Maximal1(c1) | - TrueIn(f4(c1),c1). [back_unit_del(73),unit_del(b,144)]. 168 - Maximal1(c1). [ur(70,a,144,a)]. 169 - TrueIn(f4(c1),c1). [back_unit_del(167),unit_del(a,168)]. 171 Property(VAC(f4(c1))). [back_unit_del(164),unit_del(a,168)]. 173 - Encp(c1,f4(c1)). [back_unit_del(162),unit_del(a,169),unit_del(c,168)]. 175 Enc(c1,VAC(f4(c1))). [back_unit_del(148),unit_del(a,168),unit_del(b,171)]. 176 $F. [back_unit_del(146),unit_del(a,173),unit_del(b,171),unit_del(c,175),unit_del(d,168)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=61. Generated=137. Kept=107. proofs=1. Usable=16. Sos=12. Demods=0. Denials=0. Limbo=8, Disabled=138. Hints=0. Megabytes=0.14. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3738 exit (max_proofs) Wed Jun 14 17:08:22 2006