============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3767 was started by zalta on mally, Wed Jun 14 17:11:43 2006 The command was "prove". ============================== 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 (6 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 25 clauses. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. ============================== PROOF ================================= % Proof 1 at 0.11 (+ 0.01) seconds. % Length of proof is 174. % Level of proof is 85. % Maximum clause weight is 26. % Given clauses 360. 1 Situation(c1). [clausify]. 2 Situation(c2). [clausify]. 4 - Situation(x) | Object(x). [clausify]. 7 - Object(x) | - Situation(x) | Ex1At(A,x,W). [clausify]. 8 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 9 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 11 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f3(x,y)). [clausify]. 16 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f3(x,y)). [clausify]. 17 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f1(x,y)). [clausify]. 18 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f3(x,y). [clausify]. 19 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f1(x,y)) = y. [clausify]. 22 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 28 - Object(c1) | Ex1At(A,c1,W). [resolve(7,b,1,a)]. 29 - Object(c2) | Ex1At(A,c2,W). [resolve(7,b,2,a)]. 30 - Object(c1) | - Property(x) | - Enc(c1,x) | Proposition(f1(c1,x)). [resolve(17,b,1,a)]. 34 - Object(c1) | - Property(x) | - Enc(c1,x) | VAC(f1(c1,x)) = x. [resolve(19,b,1,a)]. 40 - Object(x) | - Proposition(y) | Property(f3(x,y)) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(11,c,8,d)]. 41 - Object(x) | - Proposition(y) | Enc(x,f3(x,y)) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(16,c,8,d)]. 42 - Object(x) | - Proposition(y) | VAC(y) = f3(x,y) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(18,c,8,d)]. 43 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | - Object(x) | - Proposition(y) | TrueIn(y,x). [resolve(22,c,9,d)]. 47 - PartOf(c1,c2) | - TrueIn(c3,c2). [clausify]. 48 - PartOf(c1,c2) | Proposition(c3). [clausify]. 49 - PartOf(c1,c2) | TrueIn(c3,c1). [clausify]. 52 PartOf(c1,c2) | - Proposition(x) | - TrueIn(x,c1) | TrueIn(x,c2). [clausify]. 53 - Object(x) | - Object(y) | - PartOf(x,y) | - Property(z) | - Enc(x,z) | Enc(y,z). [clausify]. 54 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | Property(f4(x,y)). [clausify]. 55 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | Enc(x,f4(x,y)). [clausify]. 56 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | - Enc(y,f4(x,y)). [clausify]. 57 Object(c1). [resolve(4,a,1,a)]. 58 Object(c2). [resolve(4,a,2,a)]. 59 Ex1At(A,c1,W). [copy(28),unit_del(a,57)]. 60 Ex1At(A,c2,W). [copy(29),unit_del(a,58)]. 61 - Property(x) | - Enc(c1,x) | Proposition(f1(c1,x)). [copy(30),unit_del(a,57)]. 65 - Property(x) | - Enc(c1,x) | VAC(f1(c1,x)) = x. [copy(34),unit_del(a,57)]. 71 - Object(x) | - Proposition(y) | Property(f3(x,y)) | - TrueIn(y,x). [copy(40),merge(d),merge(e)]. 72 - Object(x) | - Proposition(y) | Enc(x,f3(x,y)) | - TrueIn(y,x). [copy(41),merge(d),merge(e)]. 73 - Object(x) | - Proposition(y) | f3(x,y) = VAC(y) | - TrueIn(y,x). [copy(42),flip(c),merge(d),merge(e)]. 74 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | TrueIn(y,x). [copy(43),merge(f),merge(g)]. 83 - Object(x) | PartOf(c1,x) | - Ex1At(A,x,W) | - Enc(x,f4(c1,x)). [resolve(59,a,56,d),unit_del(a,57)]. 85 - Object(x) | PartOf(c1,x) | - Ex1At(A,x,W) | Enc(c1,f4(c1,x)). [resolve(59,a,55,d),unit_del(a,57)]. 87 - Object(x) | PartOf(c1,x) | - Ex1At(A,x,W) | Property(f4(c1,x)). [resolve(59,a,54,d),unit_del(a,57)]. 105 PartOf(c1,c2) | - Enc(c2,f4(c1,c2)). [resolve(83,c,60,a),unit_del(a,58)]. 108 PartOf(c1,c2) | Enc(c1,f4(c1,c2)). [resolve(85,c,60,a),unit_del(a,58)]. 109 Enc(c1,f4(c1,c2)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(108,a,53,c),unit_del(b,57),unit_del(c,58)]. 110 Enc(c1,f4(c1,c2)) | TrueIn(c3,c1). [resolve(108,a,49,a)]. 111 Enc(c1,f4(c1,c2)) | Proposition(c3). [resolve(108,a,48,a)]. 113 Enc(c1,f4(c1,c2)) | - Proposition(c3) | VAC(c3) = f3(c1,c3). [resolve(110,b,73,d),flip(d),unit_del(b,57)]. 114 Enc(c1,f4(c1,c2)) | - Proposition(c3) | Enc(c1,f3(c1,c3)). [resolve(110,b,72,d),unit_del(b,57)]. 115 Enc(c1,f4(c1,c2)) | - Proposition(c3) | Property(f3(c1,c3)). [resolve(110,b,71,d),unit_del(b,57)]. 116 Proposition(c3) | - Property(f4(c1,c2)) | VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(111,a,65,b)]. 117 Proposition(c3) | - Property(f4(c1,c2)) | Proposition(f1(c1,f4(c1,c2))). [resolve(111,a,61,b)]. 119 PartOf(c1,c2) | Property(f4(c1,c2)). [resolve(87,c,60,a),unit_del(a,58)]. 120 Property(f4(c1,c2)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(119,a,53,c),unit_del(b,57),unit_del(c,58)]. 121 Property(f4(c1,c2)) | TrueIn(c3,c1). [resolve(119,a,49,a)]. 122 Property(f4(c1,c2)) | Proposition(c3). [resolve(119,a,48,a)]. 123 Property(f4(c1,c2)) | - Proposition(c3) | VAC(c3) = f3(c1,c3). [resolve(121,b,73,d),flip(d),unit_del(b,57)]. 124 Property(f4(c1,c2)) | - Proposition(c3) | Enc(c1,f3(c1,c3)). [resolve(121,b,72,d),unit_del(b,57)]. 125 Property(f4(c1,c2)) | - Proposition(c3) | Property(f3(c1,c3)). [resolve(121,b,71,d),unit_del(b,57)]. 126 Proposition(c3) | Proposition(f1(c1,f4(c1,c2))). [resolve(117,b,122,a),merge(c)]. 127 Proposition(c3) | VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(116,b,122,a),merge(c)]. 131 Proposition(c3) | - Object(x) | - Proposition(f1(c1,f4(c1,c2))) | - Property(f4(c1,c2)) | - Enc(x,f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),x). [resolve(127,b,74,d)]. 146 Proposition(c3) | - Proposition(f1(c1,f4(c1,c2))) | - Property(f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(131,e,111,a),merge(f),unit_del(b,57)]. 147 Proposition(c3) | - Proposition(f1(c1,f4(c1,c2))) | TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(146,c,122,a),merge(d)]. 148 Proposition(c3) | TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(147,b,126,b),merge(c)]. 152 Proposition(c3) | PartOf(c1,c2) | - Proposition(f1(c1,f4(c1,c2))) | TrueIn(f1(c1,f4(c1,c2)),c2). [resolve(148,b,52,c)]. 153 Proposition(c3) | PartOf(c1,c2) | TrueIn(f1(c1,f4(c1,c2)),c2). [resolve(152,c,126,b),merge(d)]. 154 Proposition(c3) | PartOf(c1,c2) | - Proposition(f1(c1,f4(c1,c2))) | VAC(f1(c1,f4(c1,c2))) = f3(c2,f1(c1,f4(c1,c2))). [resolve(153,c,73,d),flip(e),unit_del(c,58)]. 155 Proposition(c3) | PartOf(c1,c2) | - Proposition(f1(c1,f4(c1,c2))) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(153,c,72,d),unit_del(c,58)]. 161 Proposition(c3) | PartOf(c1,c2) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(155,c,126,b),merge(d)]. 164 Proposition(c3) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(161,b,48,a),merge(c)]. 195 Proposition(c3) | PartOf(c1,c2) | VAC(f1(c1,f4(c1,c2))) = f3(c2,f1(c1,f4(c1,c2))). [resolve(154,c,126,b),merge(d)]. 206 Proposition(c3) | PartOf(c1,c2) | f3(c2,f1(c1,f4(c1,c2))) = f4(c1,c2). [para(195(c,1),127(b,1)),merge(c)]. 218 Proposition(c3) | PartOf(c1,c2) | Enc(c2,f4(c1,c2)). [para(206(c,1),164(b,2)),merge(c)]. 221 Proposition(c3) | Enc(c2,f4(c1,c2)). [resolve(218,b,48,a),merge(c)]. 225 Proposition(c3) | PartOf(c1,c2). [resolve(221,b,105,b)]. 230 Proposition(c3). [resolve(225,b,48,a),merge(b)]. 231 Property(f4(c1,c2)) | Property(f3(c1,c3)). [back_unit_del(125),unit_del(b,230)]. 232 Property(f4(c1,c2)) | Enc(c1,f3(c1,c3)). [back_unit_del(124),unit_del(b,230)]. 233 Property(f4(c1,c2)) | VAC(c3) = f3(c1,c3). [back_unit_del(123),unit_del(b,230)]. 234 Enc(c1,f4(c1,c2)) | Property(f3(c1,c3)). [back_unit_del(115),unit_del(b,230)]. 235 Enc(c1,f4(c1,c2)) | Enc(c1,f3(c1,c3)). [back_unit_del(114),unit_del(b,230)]. 236 Enc(c1,f4(c1,c2)) | VAC(c3) = f3(c1,c3). [back_unit_del(113),unit_del(b,230)]. 237 Property(f4(c1,c2)) | - Property(f3(c1,c3)) | Enc(c2,f3(c1,c3)). [resolve(232,b,120,c),merge(b)]. 240 Property(f3(c1,c3)) | - Property(f4(c1,c2)) | VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(234,a,65,b)]. 241 Property(f3(c1,c3)) | - Property(f4(c1,c2)) | Proposition(f1(c1,f4(c1,c2))). [resolve(234,a,61,b)]. 242 Enc(c1,f3(c1,c3)) | - Property(f4(c1,c2)) | VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(235,a,65,b)]. 243 Enc(c1,f3(c1,c3)) | - Property(f4(c1,c2)) | Proposition(f1(c1,f4(c1,c2))). [resolve(235,a,61,b)]. 247 Property(f4(c1,c2)) | - Object(x) | - Property(f3(c1,c3)) | - Enc(x,f3(c1,c3)) | TrueIn(c3,x). [resolve(233,b,74,d),unit_del(c,230)]. 265 Enc(c1,f4(c1,c2)) | - Object(x) | - Property(f3(c1,c3)) | - Enc(x,f3(c1,c3)) | TrueIn(c3,x). [resolve(236,b,74,d),unit_del(c,230)]. 280 Property(f3(c1,c3)) | Proposition(f1(c1,f4(c1,c2))). [resolve(241,b,231,a),merge(c)]. 283 Proposition(f1(c1,f4(c1,c2))) | Property(f4(c1,c2)) | Enc(c2,f3(c1,c3)). [resolve(280,a,237,b)]. 286 Property(f3(c1,c3)) | VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(240,b,231,a),merge(c)]. 290 Property(f3(c1,c3)) | - Object(x) | - Proposition(f1(c1,f4(c1,c2))) | - Property(f4(c1,c2)) | - Enc(x,f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),x). [resolve(286,b,74,d)]. 305 Property(f4(c1,c2)) | - Property(f3(c1,c3)) | TrueIn(c3,c2) | Proposition(f1(c1,f4(c1,c2))). [resolve(247,d,283,c),merge(f),unit_del(b,58)]. 306 Property(f4(c1,c2)) | TrueIn(c3,c2) | Proposition(f1(c1,f4(c1,c2))). [resolve(305,b,280,a),merge(d)]. 310 Property(f4(c1,c2)) | Proposition(f1(c1,f4(c1,c2))) | - PartOf(c1,c2). [resolve(306,b,47,b)]. 311 Property(f4(c1,c2)) | Proposition(f1(c1,f4(c1,c2))). [resolve(310,c,119,a),merge(c)]. 312 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f3(c1,c3)). [resolve(311,a,243,b),merge(c)]. 313 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f4(c1,c2)) | - Property(f3(c1,c3)) | Enc(c2,f3(c1,c3)). [resolve(312,b,109,c)]. 316 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f4(c1,c2)) | Enc(c2,f3(c1,c3)). [resolve(313,c,280,a),merge(d)]. 318 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f4(c1,c2)) | - Property(f3(c1,c3)) | TrueIn(c3,c2). [resolve(316,c,265,d),merge(c),unit_del(c,58)]. 321 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f4(c1,c2)) | TrueIn(c3,c2). [resolve(318,c,280,a),merge(d)]. 325 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f4(c1,c2)) | - PartOf(c1,c2). [resolve(321,c,47,b)]. 326 Proposition(f1(c1,f4(c1,c2))) | Enc(c1,f4(c1,c2)). [resolve(325,c,108,a),merge(c)]. 328 Proposition(f1(c1,f4(c1,c2))) | - Property(f4(c1,c2)). [resolve(326,b,61,b),merge(c)]. 329 Proposition(f1(c1,f4(c1,c2))). [resolve(328,b,311,a),merge(b)]. 344 Property(f3(c1,c3)) | - Object(x) | - Property(f4(c1,c2)) | - Enc(x,f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),x). [back_unit_del(290),unit_del(c,329)]. 359 Property(f3(c1,c3)) | - Property(f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(344,d,234,a),merge(e),unit_del(b,57)]. 360 Property(f3(c1,c3)) | TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(359,b,231,a),merge(c)]. 364 Property(f3(c1,c3)) | PartOf(c1,c2) | TrueIn(f1(c1,f4(c1,c2)),c2). [resolve(360,b,52,c),unit_del(c,329)]. 365 Property(f3(c1,c3)) | PartOf(c1,c2) | VAC(f1(c1,f4(c1,c2))) = f3(c2,f1(c1,f4(c1,c2))). [resolve(364,c,73,d),flip(e),unit_del(c,58),unit_del(d,329)]. 366 Property(f3(c1,c3)) | PartOf(c1,c2) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(364,c,72,d),unit_del(c,58),unit_del(d,329)]. 373 Property(f3(c1,c3)) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))) | TrueIn(c3,c1). [resolve(366,b,49,a)]. 379 Property(f3(c1,c3)) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(373,c,71,d),merge(e),unit_del(c,57),unit_del(d,230)]. 431 Property(f3(c1,c3)) | PartOf(c1,c2) | f3(c2,f1(c1,f4(c1,c2))) = f4(c1,c2). [para(365(c,1),286(b,1)),merge(c)]. 439 Property(f3(c1,c3)) | PartOf(c1,c2) | Enc(c2,f4(c1,c2)). [para(431(c,1),379(b,2)),merge(c)]. 441 Property(f3(c1,c3)) | Enc(c2,f4(c1,c2)) | TrueIn(c3,c1). [resolve(439,b,49,a)]. 447 Property(f3(c1,c3)) | Enc(c2,f4(c1,c2)). [resolve(441,c,71,d),merge(e),unit_del(c,57),unit_del(d,230)]. 451 Property(f3(c1,c3)) | PartOf(c1,c2). [resolve(447,b,105,b)]. 455 Property(f3(c1,c3)) | TrueIn(c3,c1). [resolve(451,b,49,a)]. 458 Property(f3(c1,c3)). [resolve(455,b,71,d),merge(d),unit_del(b,57),unit_del(c,230)]. 463 Enc(c1,f4(c1,c2)) | - Object(x) | - Enc(x,f3(c1,c3)) | TrueIn(c3,x). [back_unit_del(265),unit_del(c,458)]. 471 Property(f4(c1,c2)) | - Object(x) | - Enc(x,f3(c1,c3)) | TrueIn(c3,x). [back_unit_del(247),unit_del(c,458)]. 477 Property(f4(c1,c2)) | Enc(c2,f3(c1,c3)). [back_unit_del(237),unit_del(b,458)]. 488 Property(f4(c1,c2)) | TrueIn(c3,c2). [resolve(471,c,477,b),merge(d),unit_del(b,58)]. 492 Property(f4(c1,c2)) | - PartOf(c1,c2). [resolve(488,b,47,b)]. 493 Property(f4(c1,c2)). [resolve(492,b,119,a),merge(b)]. 494 Enc(c1,f3(c1,c3)) | VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [back_unit_del(242),unit_del(b,493)]. 498 Enc(c1,f3(c1,c3)) | - Object(x) | - Enc(x,f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),x). [resolve(494,b,74,d),unit_del(c,329),unit_del(d,493)]. 509 Enc(c1,f3(c1,c3)) | TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(498,c,235,a),merge(d),unit_del(b,57)]. 513 Enc(c1,f3(c1,c3)) | PartOf(c1,c2) | TrueIn(f1(c1,f4(c1,c2)),c2). [resolve(509,b,52,c),unit_del(c,329)]. 514 Enc(c1,f3(c1,c3)) | PartOf(c1,c2) | VAC(f1(c1,f4(c1,c2))) = f3(c2,f1(c1,f4(c1,c2))). [resolve(513,c,73,d),flip(e),unit_del(c,58),unit_del(d,329)]. 515 Enc(c1,f3(c1,c3)) | PartOf(c1,c2) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(513,c,72,d),unit_del(c,58),unit_del(d,329)]. 523 Enc(c1,f3(c1,c3)) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))) | TrueIn(c3,c1). [resolve(515,b,49,a)]. 528 Enc(c1,f3(c1,c3)) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(523,c,72,d),merge(e),unit_del(c,57),unit_del(d,230)]. 655 Enc(c1,f3(c1,c3)) | PartOf(c1,c2) | f3(c2,f1(c1,f4(c1,c2))) = f4(c1,c2). [para(514(c,1),494(b,1)),merge(c)]. 658 Enc(c1,f3(c1,c3)) | PartOf(c1,c2) | Enc(c2,f4(c1,c2)). [para(655(c,1),528(b,2)),merge(c)]. 661 Enc(c1,f3(c1,c3)) | Enc(c2,f4(c1,c2)) | TrueIn(c3,c1). [resolve(658,b,49,a)]. 664 Enc(c1,f3(c1,c3)) | Enc(c2,f4(c1,c2)). [resolve(661,c,72,d),merge(e),unit_del(c,57),unit_del(d,230)]. 667 Enc(c1,f3(c1,c3)) | PartOf(c1,c2). [resolve(664,b,105,b)]. 671 Enc(c1,f3(c1,c3)) | TrueIn(c3,c1). [resolve(667,b,49,a)]. 673 Enc(c1,f3(c1,c3)). [resolve(671,b,72,d),merge(d),unit_del(b,57),unit_del(c,230)]. 674 Enc(c1,f4(c1,c2)) | Enc(c2,f3(c1,c3)). [resolve(673,a,109,c),unit_del(b,458)]. 675 VAC(f1(c1,f3(c1,c3))) = f3(c1,c3). [resolve(673,a,65,b),unit_del(a,458)]. 676 Proposition(f1(c1,f3(c1,c3))). [resolve(673,a,61,b),unit_del(a,458)]. 690 Enc(c1,f4(c1,c2)) | TrueIn(c3,c2). [resolve(674,b,463,c),merge(b),unit_del(b,58)]. 693 Enc(c1,f4(c1,c2)) | - PartOf(c1,c2). [resolve(690,b,47,b)]. 695 Enc(c1,f4(c1,c2)). [resolve(693,b,108,a),merge(b)]. 696 VAC(f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(695,a,65,b),unit_del(a,493)]. 703 - Object(x) | - Enc(x,f3(c1,c3)) | TrueIn(f1(c1,f3(c1,c3)),x). [resolve(675,a,74,d),unit_del(b,676),unit_del(c,458)]. 714 - Object(x) | - Enc(x,f4(c1,c2)) | TrueIn(f1(c1,f4(c1,c2)),x). [resolve(696,a,74,d),unit_del(b,329),unit_del(c,493)]. 721 TrueIn(f1(c1,f3(c1,c3)),c1). [resolve(703,b,673,a),unit_del(a,57)]. 723 PartOf(c1,c2) | TrueIn(f1(c1,f3(c1,c3)),c2). [resolve(721,a,52,c),unit_del(b,676)]. 724 PartOf(c1,c2) | f3(c2,f1(c1,f3(c1,c3))) = f3(c1,c3). [resolve(723,b,73,d),demod(675(24)),unit_del(b,58),unit_del(c,676)]. 725 PartOf(c1,c2) | Enc(c2,f3(c2,f1(c1,f3(c1,c3)))). [resolve(723,b,72,d),unit_del(b,58),unit_del(c,676)]. 728 TrueIn(f1(c1,f4(c1,c2)),c1). [resolve(714,b,695,a),unit_del(a,57)]. 730 PartOf(c1,c2) | TrueIn(f1(c1,f4(c1,c2)),c2). [resolve(728,a,52,c),unit_del(b,329)]. 731 PartOf(c1,c2) | f3(c2,f1(c1,f4(c1,c2))) = f4(c1,c2). [resolve(730,b,73,d),demod(696(24)),unit_del(b,58),unit_del(c,329)]. 732 PartOf(c1,c2) | Enc(c2,f3(c2,f1(c1,f4(c1,c2)))). [resolve(730,b,72,d),unit_del(b,58),unit_del(c,329)]. 734 Enc(c2,f3(c2,f1(c1,f3(c1,c3)))) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(725,a,53,c),unit_del(b,57),unit_del(c,58)]. 739 Enc(c2,f3(c2,f1(c1,f4(c1,c2)))) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(732,a,53,c),unit_del(b,57),unit_del(c,58)]. 803 Enc(c2,f3(c2,f1(c1,f3(c1,c3)))) | Enc(c2,f3(c1,c3)). [resolve(734,c,673,a),unit_del(b,458)]. 818 PartOf(c1,c2) | Enc(c2,f3(c1,c3)). [para(724(b,1),803(a,2)),merge(c)]. 819 Enc(c2,f3(c1,c3)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(818,a,53,c),unit_del(b,57),unit_del(c,58)]. 821 Enc(c2,f3(c1,c3)). [factor(819,a,d),unit_del(b,458),unit_del(c,673)]. 846 Enc(c2,f3(c2,f1(c1,f4(c1,c2)))) | Enc(c2,f4(c1,c2)). [resolve(739,c,695,a),unit_del(b,493)]. 851 PartOf(c1,c2) | Enc(c2,f4(c1,c2)). [para(731(b,1),846(a,2)),merge(c)]. 852 Enc(c2,f4(c1,c2)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(851,a,53,c),unit_del(b,57),unit_del(c,58)]. 854 Enc(c2,f4(c1,c2)). [factor(852,a,d),unit_del(b,493),unit_del(c,695)]. 856 PartOf(c1,c2). [back_unit_del(105),unit_del(b,854)]. 858 TrueIn(c3,c1). [back_unit_del(49),unit_del(a,856)]. 859 - TrueIn(c3,c2). [back_unit_del(47),unit_del(a,856)]. 860 VAC(c3) != f3(c1,c3). [ur(74,a,58,a,b,230,a,c,458,a,e,821,a,f,859,a)]. 863 $F. [resolve(858,a,73,d),flip(c),unit_del(a,57),unit_del(b,230),unit_del(c,860)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=360. Generated=1456. Kept=816. proofs=1. Usable=101. Sos=15. Demods=8. Denials=0. Limbo=0, Disabled=746. Hints=0. Megabytes=0.44. User_CPU=0.12, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3767 exit (max_proofs) Wed Jun 14 17:11:43 2006