============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3667 was started by zalta on mally, Wed Jun 14 16:56:25 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). % formulas(sos). % not echoed (7 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <176,73>. Problem reduction (0.00 sec) gives one subproblem (<324,65>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 30 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.26 (+ 0.02) seconds. % Length of proof is 204. % Level of proof is 130. % Maximum clause weight is 57. % Given clauses 608. 31 Property(c1). [clausify]. 32 Object(c2). [clausify]. 33 Object(c3). [clausify]. 34 Enc(c2,c1). [clausify]. 35 Enc(c3,c1). [clausify]. 37 - IsTheFormOf(x,c1) | - PartPH(c2,x) | - PartPH(c3,x). [clausify]. 38 - Property(x) | Object(f2(x)). [clausify]. 39 - IsAFormOf(x,y) | Object(x). [clausify]. 41 - Property(x) | Ex1(A,f2(x),W). [clausify]. 43 - Object(x) | - Property(y) | - IsAFormOf(x,y) | Ex1(A,x,W). [clausify]. 44 - Property(x) | - Property(y) | - Enc(f2(x),y) | Implies(x,y). [clausify]. 45 - Property(x) | - Property(y) | Enc(f2(x),y) | - Implies(x,y). [clausify]. 50 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | - Enc(x,z) | Implies(y,z). [clausify]. 51 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | Enc(x,z) | - Implies(y,z). [clausify]. 52 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Property(f1(x,y)). [clausify]. 53 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - IsTheFormOf(y,z) | - Enc(x,z). [clausify]. 54 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y). [clausify]. 55 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f5(x,y) != x. [clausify]. 56 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f3(x,y)) | y = x. [clausify]. 57 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Enc(x,f1(x,y)) | Implies(y,f1(x,y)). [clausify]. 58 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | - Enc(x,f1(x,y)) | - Implies(y,f1(x,y)). [clausify]. 59 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f3(x,y)) | Enc(y,f3(x,y)) | y = x. [clausify]. 60 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f3(x,y)) | - Enc(y,f3(x,y)) | y = x. [clausify]. 69 Object(f2(c1)). [resolve(38,a,31,a)]. 70 Ex1(A,f2(c1),W). [resolve(41,a,31,a)]. 72 - Object(x) | - Ex1(A,x,W) | - Enc(f2(c1),f3(f2(c1),x)) | - Enc(x,f3(f2(c1),x)) | f2(c1) = x. [resolve(70,a,60,c),flip(f),unit_del(a,69)]. 74 - Object(x) | - Ex1(A,x,W) | Enc(f2(c1),f3(f2(c1),x)) | Enc(x,f3(f2(c1),x)) | f2(c1) = x. [resolve(70,a,59,c),flip(f),unit_del(a,69)]. 75 - Property(x) | IsAFormOf(f2(c1),x) | - Enc(f2(c1),f1(f2(c1),x)) | - Implies(x,f1(f2(c1),x)). [resolve(70,a,58,d),unit_del(a,69)]. 76 - Property(x) | IsAFormOf(f2(c1),x) | Enc(f2(c1),f1(f2(c1),x)) | Implies(x,f1(f2(c1),x)). [resolve(70,a,57,d),unit_del(a,69)]. 78 - Object(x) | - Ex1(A,x,W) | Property(f3(f2(c1),x)) | f2(c1) = x. [resolve(70,a,56,c),flip(e),unit_del(a,69)]. 79 - Property(x) | IsAFormOf(f2(c1),x) | Property(f1(f2(c1),x)). [resolve(70,a,52,d),unit_del(a,69)]. 80 IsAFormOf(f2(c1),c1) | Property(f1(f2(c1),c1)). [resolve(79,a,31,a)]. 82 Property(f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(80,a,54,d),unit_del(b,69),unit_del(c,31)]. 83 Property(f1(f2(c1),c1)) | - Property(x) | - Enc(f2(c1),x) | Implies(c1,x). [resolve(80,a,50,c),unit_del(b,69),unit_del(c,31)]. 85 Property(f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(82,b,53,e),unit_del(d,69),unit_del(f,31)]. 87 Property(f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c3,f2(c1)). [resolve(85,e,35,a),unit_del(c,33)]. 88 Property(f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c2,f2(c1)). [resolve(85,e,34,a),unit_del(c,32)]. 92 Property(f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(87,c,37,c)]. 96 Property(f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(92,d,88,c),merge(d),merge(e)]. 97 Property(f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(96,c,82,b),merge(c),merge(d)]. 100 Property(f1(f2(c1),c1)) | - Object(f5(f2(c1),c1)) | - Property(x) | - Enc(f5(f2(c1),c1),x) | Implies(c1,x). [resolve(97,b,50,c),unit_del(c,31)]. 101 Property(f1(f2(c1),c1)) | - Object(f5(f2(c1),c1)) | Ex1(A,f5(f2(c1),c1),W). [resolve(97,b,43,c),unit_del(c,31)]. 102 Property(f1(f2(c1),c1)) | Object(f5(f2(c1),c1)). [resolve(97,b,39,a)]. 107 IsAFormOf(f2(c1),c1) | Enc(f2(c1),f1(f2(c1),c1)) | Implies(c1,f1(f2(c1),c1)). [resolve(76,a,31,a)]. 109 IsAFormOf(f2(c1),c1) | Enc(f2(c1),f1(f2(c1),c1)) | - Property(f1(f2(c1),c1)). [resolve(107,c,45,d),merge(e),unit_del(c,31)]. 110 IsAFormOf(f2(c1),c1) | Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)). [resolve(109,c,102,a)]. 112 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(110,a,54,d),unit_del(c,69),unit_del(d,31)]. 115 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(112,c,53,e),unit_del(e,69),unit_del(g,31)]. 135 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c3,f2(c1)). [resolve(115,f,35,a),unit_del(d,33)]. 136 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c2,f2(c1)). [resolve(115,f,34,a),unit_del(d,32)]. 140 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(135,d,37,c)]. 146 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(140,e,136,d),merge(e),merge(f),merge(g)]. 147 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(146,d,112,c),merge(d),merge(e),merge(f)]. 148 Enc(f2(c1),f1(f2(c1),c1)) | Object(f5(f2(c1),c1)). [resolve(147,c,39,a),merge(c)]. 149 Object(f5(f2(c1),c1)) | - Property(f1(f2(c1),c1)) | Implies(c1,f1(f2(c1),c1)). [resolve(148,a,44,c),unit_del(b,31)]. 151 Object(f5(f2(c1),c1)) | Implies(c1,f1(f2(c1),c1)). [resolve(149,b,102,a),merge(c)]. 152 Object(f5(f2(c1),c1)) | IsAFormOf(f2(c1),c1) | - Enc(f2(c1),f1(f2(c1),c1)). [resolve(151,b,75,d),unit_del(b,31)]. 154 Object(f5(f2(c1),c1)) | IsAFormOf(f2(c1),c1). [resolve(152,c,148,a),merge(c)]. 156 Object(f5(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(154,b,54,d),unit_del(b,69),unit_del(c,31)]. 160 Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(156,b,53,e),unit_del(d,69),unit_del(f,31)]. 163 Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c3,f2(c1)). [resolve(160,e,35,a),unit_del(c,33)]. 164 Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c2,f2(c1)). [resolve(160,e,34,a),unit_del(c,32)]. 168 Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(163,c,37,c)]. 173 Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(168,d,164,c),merge(d),merge(e)]. 174 Object(f5(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(173,c,156,b),merge(c),merge(d)]. 175 Object(f5(f2(c1),c1)). [resolve(174,b,39,a),merge(b)]. 176 Property(f1(f2(c1),c1)) | Ex1(A,f5(f2(c1),c1),W). [back_unit_del(101),unit_del(b,175)]. 177 Property(f1(f2(c1),c1)) | - Property(x) | - Enc(f5(f2(c1),c1),x) | Implies(c1,x). [back_unit_del(100),unit_del(b,175)]. 180 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(176,b,78,b),flip(d),unit_del(b,175)]. 182 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(176,b,74,b),flip(e),unit_del(b,175)]. 184 Property(f1(f2(c1),c1)) | - Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | - Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(176,b,72,b),flip(e),unit_del(b,175)]. 198 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(180,c,55,e),unit_del(c,69),unit_del(d,31)]. 202 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(198,d,80,a),merge(d)]. 204 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(202,c,53,e),unit_del(d,69),unit_del(f,31)]. 210 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(182,d,55,e),unit_del(d,69),unit_del(e,31)]. 273 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | PartPH(c3,f2(c1)). [resolve(204,e,35,a),unit_del(c,33)]. 274 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | PartPH(c2,f2(c1)). [resolve(204,e,34,a),unit_del(c,32)]. 278 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(273,c,37,c)]. 282 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(278,d,274,c),merge(d),merge(e)]. 284 Property(f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))). [resolve(282,c,202,c),merge(c),merge(d)]. 334 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(210,e,80,a),merge(e)]. 560 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(334,d,53,e),unit_del(e,69),unit_del(g,31)]. 573 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | PartPH(c3,f2(c1)). [resolve(560,f,35,a),unit_del(d,33)]. 574 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | PartPH(c2,f2(c1)). [resolve(560,f,34,a),unit_del(d,32)]. 578 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(573,d,37,c)]. 583 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(578,e,574,d),merge(e),merge(f),merge(g)]. 585 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(583,d,334,d),merge(d),merge(e),merge(f)]. 586 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | - Property(f3(f2(c1),f5(f2(c1),c1))) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(585,c,177,c),merge(c)]. 610 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(586,c,284,b),merge(d)]. 615 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | - Property(f3(f2(c1),f5(f2(c1),c1))). [resolve(610,c,45,d),merge(e),unit_del(c,31)]. 616 Property(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(615,c,284,b),merge(c)]. 617 Property(f1(f2(c1),c1)) | - Property(f3(f2(c1),f5(f2(c1),c1))) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(616,b,83,c),merge(b)]. 618 Property(f1(f2(c1),c1)) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(617,b,284,b),merge(c)]. 619 Property(f1(f2(c1),c1)) | - Object(x) | - IsAFormOf(x,c1) | - Property(f3(f2(c1),f5(f2(c1),c1))) | Enc(x,f3(f2(c1),f5(f2(c1),c1))). [resolve(618,b,51,f),unit_del(c,31)]. 621 Property(f1(f2(c1),c1)) | - Property(f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(619,c,97,b),merge(e),unit_del(b,175)]. 622 Property(f1(f2(c1),c1)) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(621,b,284,b),merge(c)]. 623 Property(f1(f2(c1),c1)) | - Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(622,b,184,c),merge(b)]. 624 Property(f1(f2(c1),c1)) | f5(f2(c1),c1) = f2(c1). [resolve(623,b,616,b),merge(c)]. 625 Property(f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(624,b,55,e),unit_del(b,69),unit_del(c,31)]. 655 Property(f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1). [resolve(625,c,80,a),merge(c)]. 657 Property(f1(f2(c1),c1)) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(655,b,53,e),unit_del(c,69),unit_del(e,31)]. 663 Property(f1(f2(c1),c1)) | PartPH(c3,f2(c1)). [resolve(657,d,35,a),unit_del(b,33)]. 664 Property(f1(f2(c1),c1)) | PartPH(c2,f2(c1)). [resolve(657,d,34,a),unit_del(b,32)]. 668 Property(f1(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(663,b,37,c)]. 674 Property(f1(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1). [resolve(668,c,664,b),merge(c)]. 675 Property(f1(f2(c1),c1)). [resolve(674,b,655,b),merge(b)]. 676 IsAFormOf(f2(c1),c1) | Enc(f2(c1),f1(f2(c1),c1)). [back_unit_del(109),unit_del(c,675)]. 682 Enc(f2(c1),f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(676,a,54,d),unit_del(b,69),unit_del(c,31)]. 683 Enc(f2(c1),f1(f2(c1),c1)) | - Property(x) | - Enc(f2(c1),x) | Implies(c1,x). [resolve(676,a,50,c),unit_del(b,69),unit_del(c,31)]. 685 Enc(f2(c1),f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(682,b,53,e),unit_del(d,69),unit_del(f,31)]. 705 Enc(f2(c1),f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c3,f2(c1)). [resolve(685,e,35,a),unit_del(c,33)]. 706 Enc(f2(c1),f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c2,f2(c1)). [resolve(685,e,34,a),unit_del(c,32)]. 712 Enc(f2(c1),f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(705,c,37,c)]. 716 Enc(f2(c1),f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(712,d,706,c),merge(d),merge(e)]. 717 Enc(f2(c1),f1(f2(c1),c1)) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(716,c,682,b),merge(c),merge(d)]. 720 Enc(f2(c1),f1(f2(c1),c1)) | - Property(x) | - Enc(f5(f2(c1),c1),x) | Implies(c1,x). [resolve(717,b,50,c),unit_del(b,175),unit_del(c,31)]. 721 Enc(f2(c1),f1(f2(c1),c1)) | Ex1(A,f5(f2(c1),c1),W). [resolve(717,b,43,c),unit_del(b,175),unit_del(c,31)]. 722 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(721,b,78,b),flip(d),unit_del(b,175)]. 724 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(721,b,74,b),flip(e),unit_del(b,175)]. 726 Enc(f2(c1),f1(f2(c1),c1)) | - Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | - Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(721,b,72,b),flip(e),unit_del(b,175)]. 743 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(722,c,55,e),unit_del(c,69),unit_del(d,31)]. 745 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(743,d,676,a),merge(d)]. 749 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(745,c,53,e),unit_del(d,69),unit_del(f,31)]. 802 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | PartPH(c3,f2(c1)). [resolve(749,e,35,a),unit_del(c,33)]. 803 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | PartPH(c2,f2(c1)). [resolve(749,e,34,a),unit_del(c,32)]. 818 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(802,c,37,c)]. 822 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(818,d,803,c),merge(d),merge(e)]. 824 Enc(f2(c1),f1(f2(c1),c1)) | Property(f3(f2(c1),f5(f2(c1),c1))). [resolve(822,c,745,c),merge(c),merge(d)]. 837 Property(f3(f2(c1),f5(f2(c1),c1))) | Implies(c1,f1(f2(c1),c1)). [resolve(824,a,44,c),unit_del(b,31),unit_del(c,675)]. 838 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f2(c1),c1) | - Enc(f2(c1),f1(f2(c1),c1)). [resolve(837,b,75,d),unit_del(b,31)]. 840 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f2(c1),c1). [resolve(838,c,824,a),merge(c)]. 842 Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(840,b,54,d),unit_del(b,69),unit_del(c,31)]. 846 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f5(f2(c1),c1),c1) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(842,b,53,e),unit_del(d,69),unit_del(f,31)]. 849 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c3,f2(c1)). [resolve(846,e,35,a),unit_del(c,33)]. 850 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c2,f2(c1)). [resolve(846,e,34,a),unit_del(c,32)]. 854 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(849,c,37,c)]. 868 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(854,d,850,c),merge(d),merge(e)]. 869 Property(f3(f2(c1),f5(f2(c1),c1))) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(868,c,842,b),merge(c),merge(d)]. 874 Property(f3(f2(c1),f5(f2(c1),c1))) | Ex1(A,f5(f2(c1),c1),W). [resolve(869,b,43,c),unit_del(b,175),unit_del(c,31)]. 881 Property(f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(874,b,78,b),flip(d),merge(c),unit_del(b,175)]. 891 Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(881,b,55,e),unit_del(b,69),unit_del(c,31)]. 892 Property(f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(891,c,840,b),merge(c)]. 897 Property(f3(f2(c1),f5(f2(c1),c1))) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(892,b,53,e),unit_del(c,69),unit_del(e,31)]. 899 Property(f3(f2(c1),f5(f2(c1),c1))) | PartPH(c3,f2(c1)). [resolve(897,d,35,a),unit_del(b,33)]. 900 Property(f3(f2(c1),f5(f2(c1),c1))) | PartPH(c2,f2(c1)). [resolve(897,d,34,a),unit_del(b,32)]. 907 Property(f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(899,b,37,c)]. 911 Property(f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(907,c,900,b),merge(c)]. 912 Property(f3(f2(c1),f5(f2(c1),c1))). [resolve(911,b,892,b),merge(b)]. 944 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(724,d,55,e),unit_del(d,69),unit_del(e,31)]. 1039 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(944,e,676,a),merge(e)]. 1041 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(1039,d,53,e),unit_del(e,69),unit_del(g,31)]. 1053 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | PartPH(c3,f2(c1)). [resolve(1041,f,35,a),unit_del(d,33)]. 1054 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | PartPH(c2,f2(c1)). [resolve(1041,f,34,a),unit_del(d,32)]. 1058 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(1053,d,37,c)]. 1062 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(1058,e,1054,d),merge(e),merge(f),merge(g)]. 1064 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(1062,d,1039,d),merge(d),merge(e),merge(f)]. 1066 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(1064,c,720,c),merge(c),unit_del(c,912)]. 1069 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(1066,c,45,d),merge(e),unit_del(c,31),unit_del(d,912)]. 1073 Enc(f2(c1),f1(f2(c1),c1)) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(1069,b,683,c),merge(b),unit_del(b,912)]. 1076 Enc(f2(c1),f1(f2(c1),c1)) | - Object(x) | - IsAFormOf(x,c1) | Enc(x,f3(f2(c1),f5(f2(c1),c1))). [resolve(1073,b,51,f),unit_del(c,31),unit_del(e,912)]. 1079 Enc(f2(c1),f1(f2(c1),c1)) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(1076,c,717,b),merge(d),unit_del(b,175)]. 1081 Enc(f2(c1),f1(f2(c1),c1)) | - Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(1079,b,726,c),merge(b)]. 1083 Enc(f2(c1),f1(f2(c1),c1)) | f5(f2(c1),c1) = f2(c1). [resolve(1081,b,1069,b),merge(c)]. 1084 Enc(f2(c1),f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(1083,b,55,e),unit_del(b,69),unit_del(c,31)]. 1102 Enc(f2(c1),f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1). [resolve(1084,c,676,a),merge(c)]. 1104 Enc(f2(c1),f1(f2(c1),c1)) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(1102,b,53,e),unit_del(c,69),unit_del(e,31)]. 1108 Enc(f2(c1),f1(f2(c1),c1)) | PartPH(c3,f2(c1)). [resolve(1104,d,35,a),unit_del(b,33)]. 1109 Enc(f2(c1),f1(f2(c1),c1)) | PartPH(c2,f2(c1)). [resolve(1104,d,34,a),unit_del(b,32)]. 1113 Enc(f2(c1),f1(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(1108,b,37,c)]. 1117 Enc(f2(c1),f1(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1). [resolve(1113,c,1109,b),merge(c)]. 1118 Enc(f2(c1),f1(f2(c1),c1)). [resolve(1117,b,1102,b),merge(b)]. 1125 Implies(c1,f1(f2(c1),c1)). [resolve(1118,a,44,c),unit_del(a,31),unit_del(b,675)]. 1126 IsAFormOf(f2(c1),c1). [resolve(1125,a,75,d),unit_del(a,31),unit_del(c,1118)]. 1131 IsTheFormOf(f2(c1),c1) | IsAFormOf(f5(f2(c1),c1),c1). [resolve(1126,a,54,d),unit_del(a,69),unit_del(b,31)]. 1132 - Property(x) | - Enc(f2(c1),x) | Implies(c1,x). [resolve(1126,a,50,c),unit_del(a,69),unit_del(b,31)]. 1134 IsAFormOf(f5(f2(c1),c1),c1) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(1131,a,53,e),unit_del(c,69),unit_del(e,31)]. 1137 IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c3,f2(c1)). [resolve(1134,d,35,a),unit_del(b,33)]. 1138 IsAFormOf(f5(f2(c1),c1),c1) | PartPH(c2,f2(c1)). [resolve(1134,d,34,a),unit_del(b,32)]. 1142 IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(1137,b,37,c)]. 1146 IsAFormOf(f5(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(1142,c,1138,b),merge(c)]. 1147 IsAFormOf(f5(f2(c1),c1),c1). [resolve(1146,b,1131,a),merge(b)]. 1153 - Property(x) | - Enc(f5(f2(c1),c1),x) | Implies(c1,x). [resolve(1147,a,50,c),unit_del(a,175),unit_del(b,31)]. 1154 Ex1(A,f5(f2(c1),c1),W). [resolve(1147,a,43,c),unit_del(a,175),unit_del(b,31)]. 1165 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(1154,a,74,b),flip(d),unit_del(a,175)]. 1167 - Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | - Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [resolve(1154,a,72,b),flip(d),unit_del(a,175)]. 1259 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(1165,c,55,e),unit_del(c,69),unit_del(d,31),unit_del(f,1126)]. 1269 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(1259,c,53,e),unit_del(d,69),unit_del(f,31)]. 1294 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | PartPH(c3,f2(c1)). [resolve(1269,e,35,a),unit_del(c,33)]. 1295 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | PartPH(c2,f2(c1)). [resolve(1269,e,34,a),unit_del(c,32)]. 1299 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPH(c2,f2(c1)). [resolve(1294,c,37,c)]. 1304 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(1299,d,1295,c),merge(d),merge(e)]. 1306 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(1304,c,1259,c),merge(c),merge(d)]. 1308 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))) | Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(1306,b,1153,b),unit_del(b,912)]. 1313 Enc(f2(c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(1308,b,45,d),merge(d),unit_del(b,31),unit_del(c,912)]. 1314 - Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))) | f5(f2(c1),c1) = f2(c1). [back_unit_del(1167),unit_del(a,1313)]. 1315 Implies(c1,f3(f2(c1),f5(f2(c1),c1))). [resolve(1313,a,1132,b),unit_del(a,912)]. 1322 - Object(x) | - IsAFormOf(x,c1) | Enc(x,f3(f2(c1),f5(f2(c1),c1))). [resolve(1315,a,51,f),unit_del(b,31),unit_del(d,912)]. 1325 Enc(f5(f2(c1),c1),f3(f2(c1),f5(f2(c1),c1))). [resolve(1322,b,1147,a),unit_del(a,175)]. 1326 f5(f2(c1),c1) = f2(c1). [back_unit_del(1314),unit_del(a,1325)]. 1342 IsTheFormOf(f2(c1),c1). [resolve(1326,a,55,e),unit_del(a,69),unit_del(b,31),unit_del(d,1126)]. 1344 - Object(x) | PartPH(x,f2(c1)) | - Enc(x,c1). [resolve(1342,a,53,e),unit_del(b,69),unit_del(d,31)]. 1348 PartPH(c3,f2(c1)). [resolve(1344,c,35,a),unit_del(a,33)]. 1349 PartPH(c2,f2(c1)). [resolve(1344,c,34,a),unit_del(a,32)]. 1353 $F. [resolve(1348,a,37,c),unit_del(a,1342),unit_del(b,1349)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=608. Generated=3212. Kept=1322. proofs=1. Usable=114. Sos=61. Demods=1. Denials=0. Limbo=3, Disabled=1174. Hints=0. Megabytes=0.74. User_CPU=0.26, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3667 exit (max_proofs) Wed Jun 14 16:56:25 2006