============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3746 was started by zalta on mally, Wed Jun 14 17:09:13 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). % formulas(sos). % not echoed (10 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 37 clauses. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. ============================== PROOF ================================= % Proof 1 at 0.05 (+ 0.01) seconds. % Length of proof is 144. % Level of proof is 56. % Maximum clause weight is 35. % Given clauses 256. 1 Object(c1). [clausify]. 7 - Ex1At(x,y,z) | Object(y). [clausify]. 8 - Ex1At(x,y,z) | Point(z). [clausify]. 14 - Object(x) | Actual(x) | - Situation(x) | Proposition(f4(x)). [clausify]. 16 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 17 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 18 - Object(x) | Actual(x) | - Situation(x) | TrueIn(f4(x),x). [clausify]. 19 - Object(x) | Actual(x) | - Situation(x) | - True(f4(x),W). [clausify]. 21 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f1(x,y)). [clausify]. 22 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Property(f3(x)). [clausify]. 24 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 25 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Enc(x,f3(x)). [clausify]. 26 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 27 - Object(x) | World(x) | - Situation(x) | - Point(y) | Proposition(f6(x,y)). [clausify]. 28 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f1(x,y). [clausify]. 34 - Object(x) | Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | VAC(y) != f3(x). [clausify]. 35 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 36 - Object(x) | World(x) | - Situation(x) | - Point(y) | TrueIn(f6(x,y),x) | True(f6(x,y),y). [clausify]. 37 - Object(x) | World(x) | - Situation(x) | - Point(y) | - TrueIn(f6(x,y),x) | - True(f6(x,y),y). [clausify]. 58 Situation(c1) | - Ex1At(A,c1,W) | Property(f3(c1)). [resolve(22,a,1,a)]. 62 Situation(c1) | - Ex1At(A,c1,W) | Enc(c1,f3(c1)). [resolve(25,a,1,a)]. 66 World(c1) | - Situation(c1) | - Point(x) | Proposition(f6(c1,x)). [resolve(27,a,1,a)]. 79 Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | VAC(y) != f3(x) | - Ex1At(z,x,u). [resolve(34,a,7,b)]. 82 World(c1) | - Situation(c1) | - Point(x) | TrueIn(f6(c1,x),c1) | True(f6(c1,x),x). [resolve(36,a,1,a)]. 84 World(c1) | - Situation(c1) | - Point(x) | - TrueIn(f6(c1,x),c1) | - True(f6(c1,x),x). [resolve(37,a,1,a)]. 101 Ex1At(A,c1,W). [clausify]. 102 - World(x) | - Actual(x). [clausify]. 103 - Proposition(x) | Property(VAC(x)). [clausify]. 106 - Property(x) | - Enc(c1,x) | Proposition(f7(x)). [clausify]. 107 - Property(x) | - Enc(c1,x) | True(f7(x),W). [clausify]. 108 - Property(x) | - Enc(c1,x) | VAC(f7(x)) = x. [clausify]. 109 - Proposition(x) | - Proposition(y) | VAC(y) != VAC(x) | y = x. [clausify]. 110 - Property(x) | Enc(c1,x) | - Proposition(y) | - True(y,W) | VAC(y) != x. [clausify]. 116 Actual(c1) | - Situation(c1) | Proposition(f4(c1)). [resolve(14,a,1,a)]. 118 - Proposition(x) | - TrueIn(x,c1) | Encp(c1,x). [resolve(16,a,1,a)]. 120 - Proposition(x) | TrueIn(x,c1) | - Encp(c1,x). [resolve(17,a,1,a)]. 122 Actual(c1) | - Situation(c1) | TrueIn(f4(c1),c1). [resolve(18,a,1,a)]. 124 Actual(c1) | - Situation(c1) | - True(f4(c1),W). [resolve(19,a,1,a)]. 126 - Proposition(x) | - Encp(c1,x) | Property(f1(c1,x)). [resolve(21,a,1,a)]. 128 Situation(c1) | Property(f3(c1)). [copy(58),unit_del(b,101)]. 130 - Proposition(x) | - Encp(c1,x) | Enc(c1,f1(c1,x)). [resolve(24,a,1,a)]. 132 Situation(c1) | Enc(c1,f3(c1)). [copy(62),unit_del(b,101)]. 134 - Actual(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,W). [resolve(26,a,1,a)]. 136 - Proposition(x) | - Encp(c1,x) | VAC(x) = f1(c1,x). [resolve(28,a,1,a)]. 147 Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | f3(x) != VAC(y) | - Ex1At(z,x,u). [copy(79),flip(d)]. 148 - Proposition(x) | Encp(c1,x) | - Property(y) | VAC(x) != y | - Enc(c1,y). [resolve(35,a,1,a)]. 150 World(c1) | - Situation(c1) | Proposition(f6(c1,x)) | - Ex1At(y,z,x). [resolve(66,c,8,b)]. 155 World(c1) | - Situation(c1) | TrueIn(f6(c1,x),c1) | True(f6(c1,x),x) | - Ex1At(y,z,x). [resolve(82,c,8,b)]. 160 World(c1) | - Situation(c1) | - TrueIn(f6(c1,x),c1) | - True(f6(c1,x),x) | - Ex1At(y,z,x). [resolve(84,c,8,b)]. 167 Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | f3(x) != VAC(y). [factor(147,b,e)]. 172 - Property(VAC(x)) | Enc(c1,VAC(x)) | - Proposition(x) | - True(x,W). [xx_res(110,e)]. 173 Situation(c1) | - Property(f3(c1)) | VAC(f7(f3(c1))) = f3(c1). [resolve(132,b,108,b)]. 175 Situation(c1) | - Property(f3(c1)) | Proposition(f7(f3(c1))). [resolve(132,b,106,b)]. 176 - Proposition(x) | Encp(c1,x) | - Property(VAC(x)) | - Enc(c1,VAC(x)). [xx_res(148,d)]. 178 World(c1) | - Situation(c1) | Proposition(f6(c1,W)). [resolve(150,d,101,a)]. 180 World(c1) | - Situation(c1) | TrueIn(f6(c1,W),c1) | True(f6(c1,W),W). [resolve(155,e,101,a)]. 182 World(c1) | - Situation(c1) | - TrueIn(f6(c1,W),c1) | - True(f6(c1,W),W). [resolve(160,e,101,a)]. 184 Situation(c1) | Proposition(f7(f3(c1))). [resolve(175,b,128,b),merge(c)]. 188 Situation(c1) | VAC(f7(f3(c1))) = f3(c1). [resolve(173,b,128,b),merge(c)]. 191 Situation(c1) | - Proposition(f7(f3(c1))). [resolve(188,b,167,d(flip)),merge(b),unit_del(b,101)]. 192 Situation(c1). [resolve(191,b,184,b),merge(b)]. 193 World(c1) | - TrueIn(f6(c1,W),c1) | - True(f6(c1,W),W). [back_unit_del(182),unit_del(b,192)]. 194 World(c1) | TrueIn(f6(c1,W),c1) | True(f6(c1,W),W). [back_unit_del(180),unit_del(b,192)]. 195 World(c1) | Proposition(f6(c1,W)). [back_unit_del(178),unit_del(b,192)]. 204 Actual(c1) | - True(f4(c1),W). [back_unit_del(124),unit_del(b,192)]. 205 Actual(c1) | TrueIn(f4(c1),c1). [back_unit_del(122),unit_del(b,192)]. 206 Actual(c1) | Proposition(f4(c1)). [back_unit_del(116),unit_del(b,192)]. 208 Actual(c1) | - Proposition(f4(c1)) | Encp(c1,f4(c1)). [resolve(205,b,118,b)]. 209 Proposition(f4(c1)) | - World(c1). [resolve(206,a,102,b)]. 210 Proposition(f6(c1,W)) | Proposition(f4(c1)). [resolve(195,a,209,b)]. 211 Proposition(f6(c1,W)) | Actual(c1) | Encp(c1,f4(c1)). [resolve(210,b,208,b)]. 213 Proposition(f6(c1,W)) | Actual(c1) | - Proposition(f4(c1)) | VAC(f4(c1)) = f1(c1,f4(c1)). [resolve(211,c,136,b)]. 214 Proposition(f6(c1,W)) | Actual(c1) | - Proposition(f4(c1)) | Enc(c1,f1(c1,f4(c1))). [resolve(211,c,130,b)]. 215 Proposition(f6(c1,W)) | Actual(c1) | - Proposition(f4(c1)) | Property(f1(c1,f4(c1))). [resolve(211,c,126,b)]. 217 World(c1) | TrueIn(f6(c1,W),c1) | - Property(VAC(f6(c1,W))) | Enc(c1,VAC(f6(c1,W))) | - Proposition(f6(c1,W)). [resolve(194,c,172,d)]. 219 Proposition(f6(c1,W)) | Actual(c1) | Enc(c1,f1(c1,f4(c1))). [resolve(214,c,210,b),merge(d)]. 222 Proposition(f6(c1,W)) | Actual(c1) | - Property(f1(c1,f4(c1))) | VAC(f7(f1(c1,f4(c1)))) = f1(c1,f4(c1)). [resolve(219,c,108,b)]. 223 Proposition(f6(c1,W)) | Actual(c1) | - Property(f1(c1,f4(c1))) | True(f7(f1(c1,f4(c1))),W). [resolve(219,c,107,b)]. 224 Proposition(f6(c1,W)) | Actual(c1) | - Property(f1(c1,f4(c1))) | Proposition(f7(f1(c1,f4(c1)))). [resolve(219,c,106,b)]. 225 Proposition(f6(c1,W)) | Actual(c1) | Property(f1(c1,f4(c1))). [resolve(215,c,210,b),merge(d)]. 226 Proposition(f6(c1,W)) | Property(f1(c1,f4(c1))) | - World(c1). [resolve(225,b,102,b)]. 227 Proposition(f6(c1,W)) | Property(f1(c1,f4(c1))). [resolve(226,c,195,a),merge(c)]. 228 Proposition(f6(c1,W)) | Actual(c1) | VAC(f4(c1)) = f1(c1,f4(c1)). [resolve(213,c,210,b),merge(d)]. 230 Proposition(f6(c1,W)) | Actual(c1) | - Proposition(x) | - Proposition(f4(c1)) | f1(c1,f4(c1)) != VAC(x) | f4(c1) = x. [para(228(c,1),109(c,1))]. 240 Proposition(f6(c1,W)) | Actual(c1) | VAC(f7(f1(c1,f4(c1)))) = f1(c1,f4(c1)). [resolve(222,c,227,b),merge(d)]. 241 Proposition(f6(c1,W)) | Actual(c1) | Proposition(f7(f1(c1,f4(c1)))). [resolve(224,c,227,b),merge(d)]. 242 Proposition(f6(c1,W)) | Proposition(f7(f1(c1,f4(c1)))) | - World(c1). [resolve(241,b,102,b)]. 243 Proposition(f6(c1,W)) | Proposition(f7(f1(c1,f4(c1)))). [resolve(242,c,195,a),merge(c)]. 245 Proposition(f6(c1,W)) | Actual(c1) | True(f7(f1(c1,f4(c1))),W). [resolve(223,c,227,b),merge(d)]. 262 Proposition(f6(c1,W)) | Actual(c1) | - Proposition(f7(f1(c1,f4(c1)))) | - Proposition(f4(c1)) | f7(f1(c1,f4(c1))) = f4(c1). [resolve(240,c,230,e(flip)),flip(g),merge(c),merge(d)]. 286 Proposition(f6(c1,W)) | Actual(c1) | - Proposition(f4(c1)) | f7(f1(c1,f4(c1))) = f4(c1). [resolve(262,c,243,b),merge(e)]. 287 Proposition(f6(c1,W)) | Actual(c1) | f7(f1(c1,f4(c1))) = f4(c1). [resolve(286,c,210,b),merge(d)]. 288 Proposition(f6(c1,W)) | Actual(c1) | True(f4(c1),W). [para(287(c,1),245(c,1)),merge(c),merge(d)]. 290 Proposition(f6(c1,W)) | Actual(c1). [resolve(288,c,204,b),merge(c)]. 291 Proposition(f6(c1,W)) | - World(c1). [resolve(290,b,102,b)]. 292 Proposition(f6(c1,W)). [resolve(291,b,195,a),merge(b)]. 293 World(c1) | TrueIn(f6(c1,W),c1) | - Property(VAC(f6(c1,W))) | Enc(c1,VAC(f6(c1,W))). [back_unit_del(217),unit_del(e,292)]. 294 Property(VAC(f6(c1,W))). [resolve(292,a,103,a)]. 295 World(c1) | TrueIn(f6(c1,W),c1) | Enc(c1,VAC(f6(c1,W))). [back_unit_del(293),unit_del(c,294)]. 298 World(c1) | TrueIn(f6(c1,W),c1) | Encp(c1,f6(c1,W)). [resolve(295,c,176,d),unit_del(c,292),unit_del(e,294)]. 307 World(c1) | TrueIn(f6(c1,W),c1). [resolve(298,c,120,c),merge(d),unit_del(c,292)]. 308 World(c1) | - Actual(c1) | True(f6(c1,W),W). [resolve(307,b,134,c),unit_del(c,292)]. 313 World(c1) | True(f6(c1,W),W) | Proposition(f4(c1)). [resolve(308,b,206,a)]. 322 World(c1) | Proposition(f4(c1)) | - TrueIn(f6(c1,W),c1). [resolve(313,b,193,c),merge(c)]. 324 World(c1) | Proposition(f4(c1)). [resolve(322,c,307,b),merge(c)]. 325 Proposition(f4(c1)). [resolve(324,a,209,b),merge(b)]. 326 Actual(c1) | Encp(c1,f4(c1)). [back_unit_del(208),unit_del(b,325)]. 334 Actual(c1) | VAC(f4(c1)) = f1(c1,f4(c1)). [resolve(326,b,136,b),unit_del(b,325)]. 335 Actual(c1) | Enc(c1,f1(c1,f4(c1))). [resolve(326,b,130,b),unit_del(b,325)]. 336 Actual(c1) | Property(f1(c1,f4(c1))). [resolve(326,b,126,b),unit_del(b,325)]. 339 Actual(c1) | - Property(f1(c1,f4(c1))) | VAC(f7(f1(c1,f4(c1)))) = f1(c1,f4(c1)). [resolve(335,b,108,b)]. 340 Actual(c1) | - Property(f1(c1,f4(c1))) | True(f7(f1(c1,f4(c1))),W). [resolve(335,b,107,b)]. 341 Actual(c1) | - Property(f1(c1,f4(c1))) | Proposition(f7(f1(c1,f4(c1)))). [resolve(335,b,106,b)]. 342 Property(f1(c1,f4(c1))) | World(c1) | True(f6(c1,W),W). [resolve(336,a,308,b)]. 343 Property(f1(c1,f4(c1))) | - World(c1). [resolve(336,a,102,b)]. 345 Actual(c1) | - Proposition(x) | f1(c1,f4(c1)) != VAC(x) | f4(c1) = x. [para(334(b,1),109(c,1)),unit_del(c,325)]. 350 Property(f1(c1,f4(c1))) | World(c1) | - TrueIn(f6(c1,W),c1). [resolve(342,c,193,c),merge(c)]. 353 Property(f1(c1,f4(c1))) | World(c1). [resolve(350,c,307,b),merge(c)]. 372 Actual(c1) | Proposition(f7(f1(c1,f4(c1)))) | World(c1). [resolve(341,b,353,a)]. 373 Proposition(f7(f1(c1,f4(c1)))) | World(c1) | True(f6(c1,W),W). [resolve(372,a,308,b),merge(c)]. 375 Proposition(f7(f1(c1,f4(c1)))) | World(c1) | - TrueIn(f6(c1,W),c1). [resolve(373,c,193,c),merge(c)]. 376 Proposition(f7(f1(c1,f4(c1)))) | World(c1). [resolve(375,c,307,b),merge(c)]. 378 Proposition(f7(f1(c1,f4(c1)))) | Property(f1(c1,f4(c1))). [resolve(376,b,343,b)]. 380 Proposition(f7(f1(c1,f4(c1)))) | Actual(c1). [resolve(378,b,341,b),merge(c)]. 381 Proposition(f7(f1(c1,f4(c1)))) | - World(c1). [resolve(380,b,102,b)]. 383 Proposition(f7(f1(c1,f4(c1)))). [resolve(381,b,376,b),merge(b)]. 385 Actual(c1) | True(f7(f1(c1,f4(c1))),W) | World(c1). [resolve(340,b,353,a)]. 386 Actual(c1) | VAC(f7(f1(c1,f4(c1)))) = f1(c1,f4(c1)) | World(c1). [resolve(339,b,353,a)]. 416 Actual(c1) | World(c1) | f7(f1(c1,f4(c1))) = f4(c1). [resolve(386,b,345,c(flip)),flip(e),merge(c),unit_del(c,383)]. 423 Actual(c1) | World(c1) | True(f4(c1),W). [para(416(c,1),385(b,1)),merge(c),merge(e)]. 440 Actual(c1) | World(c1). [resolve(423,c,204,b),merge(c)]. 441 World(c1) | True(f6(c1,W),W). [resolve(440,a,308,b),merge(b)]. 443 World(c1) | - TrueIn(f6(c1,W),c1). [resolve(441,b,193,c),merge(b)]. 444 World(c1). [resolve(443,b,307,b),merge(b)]. 445 Property(f1(c1,f4(c1))). [back_unit_del(343),unit_del(b,444)]. 452 Actual(c1) | True(f7(f1(c1,f4(c1))),W). [back_unit_del(340),unit_del(b,445)]. 453 Actual(c1) | VAC(f7(f1(c1,f4(c1)))) = f1(c1,f4(c1)). [back_unit_del(339),unit_del(b,445)]. 455 - Actual(c1). [ur(102,a,444,a)]. 457 VAC(f7(f1(c1,f4(c1)))) = f1(c1,f4(c1)). [back_unit_del(453),unit_del(a,455)]. 458 True(f7(f1(c1,f4(c1))),W). [back_unit_del(452),unit_del(a,455)]. 464 - Proposition(x) | f1(c1,f4(c1)) != VAC(x) | f4(c1) = x. [back_unit_del(345),unit_del(a,455)]. 469 - True(f4(c1),W). [back_unit_del(204),unit_del(a,455)]. 475 f7(f1(c1,f4(c1))) = f4(c1). [resolve(457,a,464,b(flip)),flip(b),unit_del(a,383)]. 476 $F. [back_demod(458),demod(475(5)),unit_del(a,469)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=256. Generated=678. Kept=375. proofs=1. Usable=78. Sos=1. Demods=4. Denials=0. Limbo=1, Disabled=395. Hints=0. Megabytes=0.43. User_CPU=0.05, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3746 exit (max_proofs) Wed Jun 14 17:09:13 2006