============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 13891 was started by zalta on mally, Sat Jul 21 17:48:31 2007 The command was "prove.orig". ============================== end of head =========================== ============================== INPUT ================================= 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 (8 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 34 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.00) seconds. % Length of proof is 137. % Level of proof is 59. % Maximum clause weight is 30. % Given clauses 217. 4 Situation(c1). [clausify]. 8 - Object(x) | - Actual(x) | Situation(x). [clausify]. 9 - Object(x) | - Situation(x) | Ex1At(A,x,W). [clausify]. 11 - Object(x) | Actual(x) | - Situation(x) | Proposition(f3(x)). [clausify]. 13 - Object(x) | Actual(x) | - Situation(x) | TrueIn(f3(x),x). [clausify]. 14 - Object(x) | Actual(x) | - Situation(x) | - True(f3(x),W). [clausify]. 15 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 16 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 19 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f4(x,y)). [clausify]. 23 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 24 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f4(x,y)). [clausify]. 25 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f1(x,y)). [clausify]. 26 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f4(x,y). [clausify]. 28 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f1(x,y)) = y. [clausify]. 31 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 35 - Object(c1) | Ex1At(A,c1,W). [resolve(9,b,4,a)]. 37 - Object(c1) | Actual(c1) | Proposition(f3(c1)). [resolve(11,c,4,a)]. 38 - Object(c1) | Actual(c1) | TrueIn(f3(c1),c1). [resolve(13,c,4,a)]. 39 - Object(c1) | Actual(c1) | - True(f3(c1),W). [resolve(14,c,4,a)]. 46 - Object(c1) | - Property(x) | - Enc(c1,x) | Proposition(f1(c1,x)). [resolve(25,b,4,a)]. 50 - Object(c1) | - Property(x) | - Enc(c1,x) | VAC(f1(c1,x)) = x. [resolve(28,b,4,a)]. 51 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f1(x,y)) = y | - Object(x) | - Actual(x). [resolve(28,b,8,c)]. 59 - Object(x) | - Actual(x) | - Proposition(y) | True(y,W) | - Object(x) | - Proposition(y) | - Encp(x,y). [resolve(23,d,16,c)]. 60 - Object(c1) | Actual(c1) | - Object(c1) | - Proposition(f3(c1)) | Encp(c1,f3(c1)). [resolve(38,c,15,c)]. 67 - Object(x) | - Actual(x) | - Proposition(y) | True(y,W) | - Object(x) | - Proposition(y) | - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z). [resolve(59,g,31,c)]. 68 - Object(c1) | Actual(c1) | - Object(c1) | - Proposition(f3(c1)) | - Object(c1) | - Proposition(f3(c1)) | Property(f4(c1,f3(c1))). [resolve(60,e,19,c)]. 69 - Object(c1) | Actual(c1) | - Object(c1) | - Proposition(f3(c1)) | - Object(c1) | - Proposition(f3(c1)) | Enc(c1,f4(c1,f3(c1))). [resolve(60,e,24,c)]. 70 - Object(c1) | Actual(c1) | - Object(c1) | - Proposition(f3(c1)) | - Object(c1) | - Proposition(f3(c1)) | VAC(f3(c1)) = f4(c1,f3(c1)). [resolve(60,e,26,c)]. 80 Object(ALPHA). [clausify]. 81 Actual(ALPHA). [clausify]. 82 Object(c1). [clausify]. 83 Ex1At(A,ALPHA,W). [clausify]. 84 Actual(c1) | PartOf(c1,ALPHA). [clausify]. 85 - Actual(c1) | - PartOf(c1,ALPHA). [clausify]. 91 - Property(x) | Enc(ALPHA,x) | - Proposition(y) | - True(y,W) | VAC(y) != x. [clausify]. 92 - Object(x) | - Object(y) | - PartOf(x,y) | - Property(z) | - Enc(x,z) | Enc(y,z). [clausify]. 93 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | Property(f5(x,y)). [clausify]. 94 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | Enc(x,f5(x,y)). [clausify]. 95 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | - Enc(y,f5(x,y)). [clausify]. 96 Ex1At(A,c1,W). [copy(35),unit_del(a,82)]. 98 Actual(c1) | Proposition(f3(c1)). [copy(37),unit_del(a,82)]. 99 Actual(c1) | - True(f3(c1),W). [copy(39),unit_del(a,82)]. 104 - Property(x) | - Enc(c1,x) | Proposition(f1(c1,x)). [copy(46),unit_del(a,82)]. 108 - Property(x) | - Enc(c1,x) | VAC(f1(c1,x)) = x. [copy(50),unit_del(a,82)]. 109 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f1(x,y)) = y | - Actual(x). [copy(51),merge(e)]. 119 - Object(x) | - Actual(x) | - Proposition(y) | True(y,W) | - Property(z) | VAC(y) != z | - Enc(x,z). [copy(67),merge(e),merge(f),merge(g),merge(h)]. 120 Actual(c1) | - Proposition(f3(c1)) | Property(f4(c1,f3(c1))). [copy(68),merge(c),merge(e),merge(f),unit_del(a,82)]. 121 Actual(c1) | - Proposition(f3(c1)) | Enc(c1,f4(c1,f3(c1))). [copy(69),merge(c),merge(e),merge(f),unit_del(a,82)]. 122 Actual(c1) | - Proposition(f3(c1)) | VAC(f3(c1)) = f4(c1,f3(c1)). [copy(70),merge(c),merge(e),merge(f),unit_del(a,82)]. 140 - Property(x) | - Enc(c1,x) | Enc(ALPHA,x) | Actual(c1). [resolve(92,c,84,b),unit_del(a,82),unit_del(b,80)]. 142 - Object(x) | PartOf(x,ALPHA) | - Ex1At(A,x,W) | Property(f5(x,ALPHA)). [resolve(93,e,83,a),unit_del(b,80)]. 148 - Object(x) | PartOf(c1,x) | - Ex1At(A,x,W) | - Enc(x,f5(c1,x)). [resolve(96,a,95,d),unit_del(a,82)]. 150 - Object(x) | PartOf(c1,x) | - Ex1At(A,x,W) | Enc(c1,f5(c1,x)). [resolve(96,a,94,d),unit_del(a,82)]. 160 - Object(x) | - Actual(x) | - Proposition(y) | True(y,W) | - Property(VAC(y)) | - Enc(x,VAC(y)). [xx_res(119,f)]. 169 PartOf(c1,ALPHA) | Property(f5(c1,ALPHA)). [resolve(142,c,96,a),unit_del(a,82)]. 171 Property(f5(c1,ALPHA)) | - Actual(c1). [resolve(169,a,85,b)]. 172 Property(f5(c1,ALPHA)) | Proposition(f3(c1)). [resolve(171,b,98,a)]. 176 PartOf(c1,ALPHA) | Enc(c1,f5(c1,ALPHA)). [resolve(150,c,83,a),unit_del(a,80)]. 178 Enc(c1,f5(c1,ALPHA)) | - Actual(c1). [resolve(176,a,85,b)]. 179 Enc(c1,f5(c1,ALPHA)) | Proposition(f3(c1)). [resolve(178,b,98,a)]. 181 Proposition(f3(c1)) | - Property(f5(c1,ALPHA)) | VAC(f1(c1,f5(c1,ALPHA))) = f5(c1,ALPHA). [resolve(179,a,108,b)]. 183 Proposition(f3(c1)) | - Property(f5(c1,ALPHA)) | Proposition(f1(c1,f5(c1,ALPHA))). [resolve(179,a,104,b)]. 184 PartOf(c1,ALPHA) | - Enc(ALPHA,f5(c1,ALPHA)). [resolve(148,c,83,a),unit_del(a,80)]. 185 Proposition(f3(c1)) | Proposition(f1(c1,f5(c1,ALPHA))). [resolve(183,b,172,a),merge(c)]. 186 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | VAC(f3(c1)) = f4(c1,f3(c1)). [resolve(185,a,122,b)]. 187 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | Enc(c1,f4(c1,f3(c1))). [resolve(185,a,121,b)]. 188 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | Property(f4(c1,f3(c1))). [resolve(185,a,120,b)]. 191 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Property(f4(c1,f3(c1))) | Enc(ALPHA,f4(c1,f3(c1))). [resolve(187,c,140,b),merge(e)]. 194 Proposition(f1(c1,f5(c1,ALPHA))) | Property(f4(c1,f3(c1))) | Enc(c1,f5(c1,ALPHA)). [resolve(188,b,178,b)]. 195 Proposition(f1(c1,f5(c1,ALPHA))) | Property(f4(c1,f3(c1))) | Property(f5(c1,ALPHA)). [resolve(188,b,171,b)]. 196 Proposition(f3(c1)) | VAC(f1(c1,f5(c1,ALPHA))) = f5(c1,ALPHA). [resolve(181,b,172,a),merge(c)]. 197 Proposition(f3(c1)) | - Object(x) | - Actual(x) | - Proposition(f1(c1,f5(c1,ALPHA))) | True(f1(c1,f5(c1,ALPHA)),W) | - Property(f5(c1,ALPHA)) | - Enc(x,f5(c1,ALPHA)). [resolve(196,b,119,f)]. 201 Proposition(f3(c1)) | - Property(f5(c1,ALPHA)) | Enc(ALPHA,f5(c1,ALPHA)) | - Proposition(f1(c1,f5(c1,ALPHA))) | - True(f1(c1,f5(c1,ALPHA)),W). [resolve(196,b,91,e)]. 243 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Object(x) | - Actual(x) | - Proposition(f3(c1)) | True(f3(c1),W) | - Property(VAC(f3(c1))) | - Enc(x,f4(c1,f3(c1))). [para(186(c,1),160(f,2))]. 249 Proposition(f1(c1,f5(c1,ALPHA))) | Property(f4(c1,f3(c1))) | - Property(f5(c1,ALPHA)). [resolve(194,c,104,b),merge(d)]. 250 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | Enc(ALPHA,f4(c1,f3(c1))) | Property(f5(c1,ALPHA)). [resolve(191,c,195,b),merge(d)]. 261 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Proposition(f3(c1)) | True(f3(c1),W) | - Property(VAC(f3(c1))) | Property(f5(c1,ALPHA)). [resolve(243,h,250,c),merge(h),merge(i),unit_del(c,80),unit_del(d,81)]. 262 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Proposition(f3(c1)) | True(f3(c1),W) | - Property(f4(c1,f3(c1))) | Property(f5(c1,ALPHA)). [para(186(c,1),261(e,1)),merge(c),merge(d)]. 264 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Proposition(f3(c1)) | True(f3(c1),W) | Property(f5(c1,ALPHA)). [resolve(262,e,195,b),merge(f),merge(g)]. 265 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | True(f3(c1),W) | Property(f5(c1,ALPHA)). [resolve(264,c,185,a),merge(e)]. 267 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | Property(f5(c1,ALPHA)). [resolve(265,c,99,b),merge(d)]. 269 Proposition(f1(c1,f5(c1,ALPHA))) | Property(f5(c1,ALPHA)). [resolve(267,b,171,b),merge(c)]. 270 Proposition(f3(c1)) | - Actual(c1) | - Proposition(f1(c1,f5(c1,ALPHA))) | True(f1(c1,f5(c1,ALPHA)),W) | - Property(f5(c1,ALPHA)). [resolve(197,g,179,a),merge(g),unit_del(b,82)]. 271 Proposition(f1(c1,f5(c1,ALPHA))) | Property(f4(c1,f3(c1))). [resolve(269,b,249,c),merge(b)]. 274 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | Enc(ALPHA,f4(c1,f3(c1))). [resolve(271,b,191,c),merge(b)]. 275 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Proposition(f3(c1)) | True(f3(c1),W) | - Property(VAC(f3(c1))). [resolve(274,c,243,h),merge(c),merge(d),unit_del(c,80),unit_del(d,81)]. 285 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Proposition(f3(c1)) | True(f3(c1),W) | - Property(f4(c1,f3(c1))). [para(186(c,1),275(e,1)),merge(c),merge(d)]. 287 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | - Proposition(f3(c1)) | True(f3(c1),W). [resolve(285,e,271,b),merge(e)]. 288 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1) | True(f3(c1),W). [resolve(287,c,185,a),merge(d)]. 290 Proposition(f1(c1,f5(c1,ALPHA))) | Actual(c1). [resolve(288,c,99,b),merge(c)]. 291 Proposition(f1(c1,f5(c1,ALPHA))) | Enc(c1,f5(c1,ALPHA)). [resolve(290,b,178,b)]. 296 Proposition(f1(c1,f5(c1,ALPHA))) | - Property(f5(c1,ALPHA)). [resolve(291,b,104,b),merge(c)]. 297 Proposition(f1(c1,f5(c1,ALPHA))). [resolve(296,b,269,b),merge(b)]. 300 Proposition(f3(c1)) | - Actual(c1) | True(f1(c1,f5(c1,ALPHA)),W) | - Property(f5(c1,ALPHA)). [back_unit_del(270),unit_del(c,297)]. 322 Proposition(f3(c1)) | - Property(f5(c1,ALPHA)) | Enc(ALPHA,f5(c1,ALPHA)) | - True(f1(c1,f5(c1,ALPHA)),W). [back_unit_del(201),unit_del(d,297)]. 327 Proposition(f3(c1)) | True(f1(c1,f5(c1,ALPHA)),W) | - Property(f5(c1,ALPHA)). [resolve(300,b,98,a),merge(d)]. 329 Proposition(f3(c1)) | True(f1(c1,f5(c1,ALPHA)),W). [resolve(327,c,172,a),merge(c)]. 331 Proposition(f3(c1)) | - Property(f5(c1,ALPHA)) | Enc(ALPHA,f5(c1,ALPHA)). [resolve(322,d,329,b),merge(d)]. 333 Proposition(f3(c1)) | Enc(ALPHA,f5(c1,ALPHA)). [resolve(331,b,172,a),merge(c)]. 334 Proposition(f3(c1)) | PartOf(c1,ALPHA). [resolve(333,b,184,b)]. 345 Proposition(f3(c1)) | - Actual(c1). [resolve(334,b,85,b)]. 346 Proposition(f3(c1)). [resolve(345,b,98,a),merge(b)]. 347 Actual(c1) | VAC(f3(c1)) = f4(c1,f3(c1)). [back_unit_del(122),unit_del(b,346)]. 348 Actual(c1) | Enc(c1,f4(c1,f3(c1))). [back_unit_del(121),unit_del(b,346)]. 349 Actual(c1) | Property(f4(c1,f3(c1))). [back_unit_del(120),unit_del(b,346)]. 352 Actual(c1) | - Property(f4(c1,f3(c1))) | Enc(ALPHA,f4(c1,f3(c1))). [resolve(348,b,140,b),merge(d)]. 355 Property(f4(c1,f3(c1))) | Enc(c1,f5(c1,ALPHA)). [resolve(349,a,178,b)]. 356 Property(f4(c1,f3(c1))) | Property(f5(c1,ALPHA)). [resolve(349,a,171,b)]. 357 Actual(c1) | - Object(x) | - Actual(x) | True(f3(c1),W) | - Property(f4(c1,f3(c1))) | - Enc(x,f4(c1,f3(c1))). [resolve(347,b,119,f),unit_del(d,346)]. 377 Actual(c1) | - Object(x) | - Actual(x) | True(f3(c1),W) | - Property(VAC(f3(c1))) | - Enc(x,f4(c1,f3(c1))). [para(347(b,1),160(f,2)),unit_del(d,346)]. 381 Property(f4(c1,f3(c1))) | - Property(f5(c1,ALPHA)) | VAC(f1(c1,f5(c1,ALPHA))) = f5(c1,ALPHA). [resolve(355,b,108,b)]. 382 Property(f5(c1,ALPHA)) | Actual(c1) | Enc(ALPHA,f4(c1,f3(c1))). [resolve(356,a,352,b)]. 392 Actual(c1) | True(f3(c1),W) | - Property(VAC(f3(c1))) | Property(f5(c1,ALPHA)). [resolve(377,f,382,c),merge(g),unit_del(b,80),unit_del(c,81)]. 394 Actual(c1) | True(f3(c1),W) | - Property(f4(c1,f3(c1))) | Property(f5(c1,ALPHA)). [para(347(b,1),392(c,1)),merge(b)]. 395 Actual(c1) | True(f3(c1),W) | Property(f5(c1,ALPHA)). [resolve(394,c,356,a),merge(d)]. 397 Actual(c1) | Property(f5(c1,ALPHA)). [resolve(395,b,99,b),merge(c)]. 399 Property(f5(c1,ALPHA)). [resolve(397,a,171,b),merge(b)]. 400 Property(f4(c1,f3(c1))) | VAC(f1(c1,f5(c1,ALPHA))) = f5(c1,ALPHA). [back_unit_del(381),unit_del(b,399)]. 401 Property(f4(c1,f3(c1))) | - Object(x) | - Actual(x) | True(f1(c1,f5(c1,ALPHA)),W) | - Enc(x,f5(c1,ALPHA)). [resolve(400,b,119,f),unit_del(d,297),unit_del(f,399)]. 405 Property(f4(c1,f3(c1))) | Enc(ALPHA,f5(c1,ALPHA)) | - True(f1(c1,f5(c1,ALPHA)),W). [resolve(400,b,91,e),unit_del(b,399),unit_del(d,297)]. 427 Property(f4(c1,f3(c1))) | - Actual(c1) | True(f1(c1,f5(c1,ALPHA)),W). [resolve(401,e,355,b),merge(e),unit_del(b,82)]. 428 Property(f4(c1,f3(c1))) | True(f1(c1,f5(c1,ALPHA)),W). [resolve(427,b,349,a),merge(c)]. 429 Property(f4(c1,f3(c1))) | Enc(ALPHA,f5(c1,ALPHA)). [resolve(428,b,405,c),merge(b)]. 431 Property(f4(c1,f3(c1))) | PartOf(c1,ALPHA). [resolve(429,b,184,b)]. 442 Property(f4(c1,f3(c1))) | - Actual(c1). [resolve(431,b,85,b)]. 443 Property(f4(c1,f3(c1))). [resolve(442,b,349,a),merge(b)]. 451 Actual(c1) | - Object(x) | - Actual(x) | True(f3(c1),W) | - Enc(x,f4(c1,f3(c1))). [back_unit_del(357),unit_del(e,443)]. 454 Actual(c1) | Enc(ALPHA,f4(c1,f3(c1))). [back_unit_del(352),unit_del(b,443)]. 464 Actual(c1) | True(f3(c1),W). [resolve(451,e,454,b),merge(e),unit_del(b,80),unit_del(c,81)]. 466 Actual(c1). [resolve(464,b,99,b),merge(b)]. 467 Enc(c1,f5(c1,ALPHA)). [back_unit_del(178),unit_del(b,466)]. 468 - PartOf(c1,ALPHA). [back_unit_del(85),unit_del(a,466)]. 469 - Enc(ALPHA,f5(c1,ALPHA)). [back_unit_del(184),unit_del(a,468)]. 470 VAC(f1(c1,f5(c1,ALPHA))) = f5(c1,ALPHA). [resolve(467,a,109,c),unit_del(a,82),unit_del(b,399),unit_del(d,466)]. 475 - True(f1(c1,f5(c1,ALPHA)),W). [resolve(470,a,91,e),unit_del(a,399),unit_del(b,469),unit_del(c,297)]. 487 - Object(x) | - Actual(x) | - Enc(x,f5(c1,ALPHA)). [para(470(a,1),160(e,1)),demod(470(25)),unit_del(c,297),unit_del(d,475),unit_del(e,399)]. 489 $F. [resolve(487,c,467,a),unit_del(a,82),unit_del(b,466)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=217. Generated=624. Kept=409. proofs=1. Usable=97. Sos=13. Demods=2. Denials=0. Limbo=0, Disabled=378. Hints=0. Megabytes=0.35. User_CPU=0.06, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13891 exit (max_proofs) Sat Jul 21 17:48:32 2007