============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3635 was started by zalta on mally, Wed Jun 14 16:56:16 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 (9 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <211,82>. Problem reduction (0.00 sec) gives one subproblem (<394,73>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 35 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.52 (+ 0.02) seconds. % Length of proof is 190. % Level of proof is 110. % Maximum clause weight is 71. % Given clauses 740. 1 Point(W). [clausify]. 31 - Object(x) | - Object(y) | - Point(z) | PartPTA(x,y,z) | - Property(u) | - IsTheFormOf(y,u) | - Ex1(u,x,z). [clausify]. 46 Property(c1). [clausify]. 47 Object(c2). [clausify]. 48 Object(c3). [clausify]. 49 Ex1(c1,c2,W). [clausify]. 50 Ex1(c1,c3,W). [clausify]. 52 - IsTheFormOf(x,c1) | - PartPTA(c2,x,W) | - PartPTA(c3,x,W). [clausify]. 53 - Property(x) | Object(f2(x)). [clausify]. 54 - IsAFormOf(x,y) | Object(x). [clausify]. 56 - Property(x) | Ex1(A,f2(x),W). [clausify]. 58 - Property(x) | - Property(y) | - Enc(f2(x),y) | Implies(x,y). [clausify]. 59 - Property(x) | - Property(y) | Enc(f2(x),y) | - Implies(x,y). [clausify]. 60 - Object(x) | - Property(y) | - IsAFormOf(x,y) | Ex1(A,x,W). [clausify]. 62 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f1(x,y),y). [clausify]. 63 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f1(x,y) != x. [clausify]. 64 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | - Enc(x,z) | Implies(y,z). [clausify]. 65 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | Enc(x,z) | - Implies(y,z). [clausify]. 66 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Property(f3(x,y)). [clausify]. 69 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f4(x,y)) | y = x. [clausify]. 70 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Enc(x,f3(x,y)) | Implies(y,f3(x,y)). [clausify]. 71 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | - Enc(x,f3(x,y)) | - Implies(y,f3(x,y)). [clausify]. 72 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f4(x,y)) | Enc(y,f4(x,y)) | y = x. [clausify]. 73 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f4(x,y)) | - Enc(y,f4(x,y)) | y = x. [clausify]. 82 - Object(x) | - Object(y) | PartPTA(x,y,W) | - Property(z) | - IsTheFormOf(y,z) | - Ex1(z,x,W). [resolve(31,c,1,a)]. 120 Object(f2(c1)). [resolve(53,a,46,a)]. 121 Ex1(A,f2(c1),W). [resolve(56,a,46,a)]. 126 - Object(x) | PartPTA(c3,x,W) | - IsTheFormOf(x,c1). [resolve(82,f,50,a),unit_del(a,48),unit_del(d,46)]. 127 - Object(x) | PartPTA(c2,x,W) | - IsTheFormOf(x,c1). [resolve(82,f,49,a),unit_del(a,47),unit_del(d,46)]. 135 - Object(x) | - Ex1(A,x,W) | - Enc(f2(c1),f4(f2(c1),x)) | - Enc(x,f4(f2(c1),x)) | f2(c1) = x. [resolve(121,a,73,c),flip(f),unit_del(a,120)]. 137 - Object(x) | - Ex1(A,x,W) | Enc(f2(c1),f4(f2(c1),x)) | Enc(x,f4(f2(c1),x)) | f2(c1) = x. [resolve(121,a,72,c),flip(f),unit_del(a,120)]. 138 - Property(x) | IsAFormOf(f2(c1),x) | - Enc(f2(c1),f3(f2(c1),x)) | - Implies(x,f3(f2(c1),x)). [resolve(121,a,71,d),unit_del(a,120)]. 139 - Property(x) | IsAFormOf(f2(c1),x) | Enc(f2(c1),f3(f2(c1),x)) | Implies(x,f3(f2(c1),x)). [resolve(121,a,70,d),unit_del(a,120)]. 141 - Object(x) | - Ex1(A,x,W) | Property(f4(f2(c1),x)) | f2(c1) = x. [resolve(121,a,69,c),flip(e),unit_del(a,120)]. 142 - Property(x) | IsAFormOf(f2(c1),x) | Property(f3(f2(c1),x)). [resolve(121,a,66,d),unit_del(a,120)]. 149 IsAFormOf(f2(c1),c1) | Property(f3(f2(c1),c1)). [resolve(142,a,46,a)]. 150 Property(f3(f2(c1),c1)) | - Property(x) | Enc(f2(c1),x) | - Implies(c1,x). [resolve(149,a,65,c),unit_del(b,120),unit_del(c,46)]. 151 Property(f3(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(149,a,62,d),unit_del(b,120),unit_del(c,46)]. 152 Property(f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c2,f2(c1),W). [resolve(151,b,127,c),unit_del(c,120)]. 153 Property(f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c3,f2(c1),W). [resolve(151,b,126,c),unit_del(c,120)]. 161 Property(f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(153,c,52,c)]. 162 Property(f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(161,d,152,c),merge(d),merge(e)]. 163 Property(f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(162,c,151,b),merge(c),merge(d)]. 165 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | - Property(x) | Enc(f1(f2(c1),c1),x) | - Implies(c1,x). [resolve(163,b,65,c),unit_del(c,46)]. 167 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | Ex1(A,f1(f2(c1),c1),W). [resolve(163,b,60,c),unit_del(c,46)]. 168 Property(f3(f2(c1),c1)) | Object(f1(f2(c1),c1)). [resolve(163,b,54,a)]. 171 Property(f3(f2(c1),c1)) | Ex1(A,f1(f2(c1),c1),W). [resolve(167,b,168,b),merge(c)]. 172 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(171,b,141,b),flip(d)]. 174 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(171,b,137,b),flip(e)]. 176 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | - Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(171,b,135,b),flip(e)]. 190 IsAFormOf(f2(c1),c1) | Enc(f2(c1),f3(f2(c1),c1)) | Implies(c1,f3(f2(c1),c1)). [resolve(139,a,46,a)]. 193 IsAFormOf(f2(c1),c1) | Implies(c1,f3(f2(c1),c1)) | - Property(f3(f2(c1),c1)). [resolve(190,b,58,c),merge(e),unit_del(c,46)]. 202 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(172,b,168,b),merge(d)]. 203 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(202,c,63,e),unit_del(c,120),unit_del(d,46)]. 211 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(203,d,149,a),merge(d)]. 212 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c2,f2(c1),W). [resolve(211,c,127,c),unit_del(c,120)]. 213 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c3,f2(c1),W). [resolve(211,c,126,c),unit_del(c,120)]. 222 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(213,c,52,c)]. 223 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(222,d,212,c),merge(d),merge(e)]. 224 Property(f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))). [resolve(223,c,211,c),merge(c),merge(d)]. 225 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(174,b,168,b),merge(e)]. 307 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(225,d,63,e),unit_del(d,120),unit_del(e,46)]. 330 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(307,e,149,a),merge(e)]. 331 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c2,f2(c1),W). [resolve(330,d,127,c),unit_del(d,120)]. 332 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c3,f2(c1),W). [resolve(330,d,126,c),unit_del(d,120)]. 344 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(332,d,52,c)]. 346 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(344,e,331,d),merge(e),merge(f),merge(g)]. 347 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(346,d,330,d),merge(d),merge(e),merge(f)]. 350 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Object(f1(f2(c1),c1)) | - Property(x) | - IsAFormOf(f1(f2(c1),c1),x) | - Property(f4(f2(c1),f1(f2(c1),c1))) | Implies(x,f4(f2(c1),f1(f2(c1),c1))). [resolve(347,c,64,e)]. 411 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Object(f1(f2(c1),c1)) | - Property(f4(f2(c1),f1(f2(c1),c1))) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(350,e,163,b),merge(g),unit_del(d,46)]. 412 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Property(f4(f2(c1),f1(f2(c1),c1))) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(411,c,168,b),merge(e)]. 413 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(412,c,224,b),merge(d)]. 416 Property(f3(f2(c1),c1)) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))) | - Property(f4(f2(c1),f1(f2(c1),c1))). [resolve(413,b,58,c),merge(e),unit_del(c,46)]. 417 Property(f3(f2(c1),c1)) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(416,c,224,b),merge(c)]. 419 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | - Property(f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(417,b,165,e),merge(b)]. 420 Property(f3(f2(c1),c1)) | - Property(f4(f2(c1),f1(f2(c1),c1))) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(417,b,150,d),merge(b)]. 423 Property(f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(420,b,224,b),merge(c)]. 442 Property(f3(f2(c1),c1)) | - Property(f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(419,b,168,b),merge(d)]. 443 Property(f3(f2(c1),c1)) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(442,b,224,b),merge(c)]. 444 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | - Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(443,b,176,d),merge(b)]. 449 Property(f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | f1(f2(c1),c1) = f2(c1). [resolve(444,c,423,b),merge(d)]. 450 Property(f3(f2(c1),c1)) | f1(f2(c1),c1) = f2(c1). [resolve(449,b,168,b),merge(c)]. 451 Property(f3(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(450,b,63,e),unit_del(b,120),unit_del(c,46)]. 514 Property(f3(f2(c1),c1)) | IsTheFormOf(f2(c1),c1). [resolve(451,c,149,a),merge(c)]. 515 Property(f3(f2(c1),c1)) | PartPTA(c2,f2(c1),W). [resolve(514,b,127,c),unit_del(b,120)]. 516 Property(f3(f2(c1),c1)) | PartPTA(c3,f2(c1),W). [resolve(514,b,126,c),unit_del(b,120)]. 524 Property(f3(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(516,b,52,c)]. 526 Property(f3(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1). [resolve(524,c,515,b),merge(c)]. 527 Property(f3(f2(c1),c1)). [resolve(526,b,514,b),merge(b)]. 528 IsAFormOf(f2(c1),c1) | Implies(c1,f3(f2(c1),c1)). [back_unit_del(193),unit_del(c,527)]. 538 Implies(c1,f3(f2(c1),c1)) | - Property(x) | Enc(f2(c1),x) | - Implies(c1,x). [resolve(528,a,65,c),unit_del(b,120),unit_del(c,46)]. 539 Implies(c1,f3(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(528,a,62,d),unit_del(b,120),unit_del(c,46)]. 544 Implies(c1,f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c2,f2(c1),W). [resolve(539,b,127,c),unit_del(c,120)]. 545 Implies(c1,f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c3,f2(c1),W). [resolve(539,b,126,c),unit_del(c,120)]. 553 Implies(c1,f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(545,c,52,c)]. 557 Implies(c1,f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(553,d,544,c),merge(d),merge(e)]. 558 Implies(c1,f3(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(557,c,539,b),merge(c),merge(d)]. 563 Implies(c1,f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | - Property(x) | Enc(f1(f2(c1),c1),x) | - Implies(c1,x). [resolve(558,b,65,c),unit_del(c,46)]. 565 Implies(c1,f3(f2(c1),c1)) | - Object(f1(f2(c1),c1)) | Ex1(A,f1(f2(c1),c1),W). [resolve(558,b,60,c),unit_del(c,46)]. 566 Implies(c1,f3(f2(c1),c1)) | Object(f1(f2(c1),c1)). [resolve(558,b,54,a)]. 569 Object(f1(f2(c1),c1)) | Enc(f2(c1),f3(f2(c1),c1)). [resolve(566,a,59,d),unit_del(b,46),unit_del(c,527)]. 579 Object(f1(f2(c1),c1)) | IsAFormOf(f2(c1),c1) | - Implies(c1,f3(f2(c1),c1)). [resolve(569,b,138,c),unit_del(b,46)]. 582 Object(f1(f2(c1),c1)) | IsAFormOf(f2(c1),c1). [resolve(579,c,566,a),merge(c)]. 589 Object(f1(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(582,b,62,d),unit_del(b,120),unit_del(c,46)]. 591 Object(f1(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c2,f2(c1),W). [resolve(589,b,127,c),unit_del(c,120)]. 592 Object(f1(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c3,f2(c1),W). [resolve(589,b,126,c),unit_del(c,120)]. 600 Object(f1(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(592,c,52,c)]. 601 Object(f1(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(600,d,591,c),merge(d),merge(e)]. 602 Object(f1(f2(c1),c1)) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(601,c,589,b),merge(c),merge(d)]. 603 Object(f1(f2(c1),c1)). [resolve(602,b,54,a),merge(b)]. 604 Implies(c1,f3(f2(c1),c1)) | Ex1(A,f1(f2(c1),c1),W). [back_unit_del(565),unit_del(b,603)]. 606 Implies(c1,f3(f2(c1),c1)) | - Property(x) | Enc(f1(f2(c1),c1),x) | - Implies(c1,x). [back_unit_del(563),unit_del(b,603)]. 627 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(604,b,141,b),flip(d),unit_del(b,603)]. 629 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(604,b,137,b),flip(e),unit_del(b,603)]. 631 Implies(c1,f3(f2(c1),c1)) | - Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(604,b,135,b),flip(e),unit_del(b,603)]. 682 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(627,c,63,e),unit_del(c,120),unit_del(d,46)]. 687 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(682,d,528,a),merge(d)]. 688 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c2,f2(c1),W). [resolve(687,c,127,c),unit_del(c,120)]. 689 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c3,f2(c1),W). [resolve(687,c,126,c),unit_del(c,120)]. 697 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(689,c,52,c)]. 698 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(697,d,688,c),merge(d),merge(e)]. 699 Implies(c1,f3(f2(c1),c1)) | Property(f4(f2(c1),f1(f2(c1),c1))). [resolve(698,c,687,c),merge(c),merge(d)]. 702 Property(f4(f2(c1),f1(f2(c1),c1))) | Enc(f2(c1),f3(f2(c1),c1)). [resolve(699,a,59,d),unit_del(b,46),unit_del(c,527)]. 709 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f2(c1),c1) | - Implies(c1,f3(f2(c1),c1)). [resolve(702,b,138,c),unit_del(b,46)]. 711 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f2(c1),c1). [resolve(709,c,699,a),merge(c)]. 713 Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(711,b,62,d),unit_del(b,120),unit_del(c,46)]. 714 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c2,f2(c1),W). [resolve(713,b,127,c),unit_del(c,120)]. 715 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c3,f2(c1),W). [resolve(713,b,126,c),unit_del(c,120)]. 724 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(715,c,52,c)]. 725 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(724,d,714,c),merge(d),merge(e)]. 726 Property(f4(f2(c1),f1(f2(c1),c1))) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(725,c,713,b),merge(c),merge(d)]. 730 Property(f4(f2(c1),f1(f2(c1),c1))) | Ex1(A,f1(f2(c1),c1),W). [resolve(726,b,60,c),unit_del(b,603),unit_del(c,46)]. 732 Property(f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(730,b,141,b),flip(d),merge(c),unit_del(b,603)]. 748 Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(732,b,63,e),unit_del(b,120),unit_del(c,46)]. 749 Property(f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(748,c,711,b),merge(c)]. 750 Property(f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c2,f2(c1),W). [resolve(749,b,127,c),unit_del(b,120)]. 751 Property(f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c3,f2(c1),W). [resolve(749,b,126,c),unit_del(b,120)]. 762 Property(f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(751,b,52,c)]. 763 Property(f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(762,c,750,b),merge(c)]. 764 Property(f4(f2(c1),f1(f2(c1),c1))). [resolve(763,b,749,b),merge(b)]. 963 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(629,d,63,e),unit_del(d,120),unit_del(e,46)]. 1362 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(963,e,528,a),merge(e)]. 1364 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c2,f2(c1),W). [resolve(1362,d,127,c),unit_del(d,120)]. 1365 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c3,f2(c1),W). [resolve(1362,d,126,c),unit_del(d,120)]. 1373 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(1365,d,52,c)]. 1411 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(1373,e,1364,d),merge(e),merge(f),merge(g)]. 1413 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(1411,d,1362,d),merge(d),merge(e),merge(f)]. 1418 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Property(x) | - IsAFormOf(f1(f2(c1),c1),x) | Implies(x,f4(f2(c1),f1(f2(c1),c1))). [resolve(1413,c,64,e),unit_del(c,603),unit_del(f,764)]. 1427 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(1418,d,558,b),merge(e),unit_del(c,46)]. 1430 Implies(c1,f3(f2(c1),c1)) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(1427,b,58,c),merge(e),unit_del(c,46),unit_del(d,764)]. 1432 Implies(c1,f3(f2(c1),c1)) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(1430,b,606,d),merge(b),unit_del(b,764)]. 1434 Implies(c1,f3(f2(c1),c1)) | Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(1430,b,538,d),merge(b),unit_del(b,764)]. 1452 Implies(c1,f3(f2(c1),c1)) | - Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(1432,b,631,c),merge(b)]. 1458 Implies(c1,f3(f2(c1),c1)) | f1(f2(c1),c1) = f2(c1). [resolve(1452,b,1434,b),merge(c)]. 1461 Implies(c1,f3(f2(c1),c1)) | IsTheFormOf(f2(c1),c1) | - IsAFormOf(f2(c1),c1). [resolve(1458,b,63,e),unit_del(b,120),unit_del(c,46)]. 1500 Implies(c1,f3(f2(c1),c1)) | IsTheFormOf(f2(c1),c1). [resolve(1461,c,528,a),merge(c)]. 1502 Implies(c1,f3(f2(c1),c1)) | PartPTA(c2,f2(c1),W). [resolve(1500,b,127,c),unit_del(b,120)]. 1503 Implies(c1,f3(f2(c1),c1)) | PartPTA(c3,f2(c1),W). [resolve(1500,b,126,c),unit_del(b,120)]. 1512 Implies(c1,f3(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(1503,b,52,c)]. 1514 Implies(c1,f3(f2(c1),c1)) | - IsTheFormOf(f2(c1),c1). [resolve(1512,c,1502,b),merge(c)]. 1515 Implies(c1,f3(f2(c1),c1)). [resolve(1514,b,1500,b),merge(b)]. 1522 Enc(f2(c1),f3(f2(c1),c1)). [resolve(1515,a,59,d),unit_del(a,46),unit_del(b,527)]. 1529 IsAFormOf(f2(c1),c1). [resolve(1522,a,138,c),unit_del(a,46),unit_del(c,1515)]. 1532 - Property(x) | Enc(f2(c1),x) | - Implies(c1,x). [resolve(1529,a,65,c),unit_del(a,120),unit_del(b,46)]. 1533 IsTheFormOf(f2(c1),c1) | IsAFormOf(f1(f2(c1),c1),c1). [resolve(1529,a,62,d),unit_del(a,120),unit_del(b,46)]. 1538 IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c2,f2(c1),W). [resolve(1533,a,127,c),unit_del(b,120)]. 1539 IsAFormOf(f1(f2(c1),c1),c1) | PartPTA(c3,f2(c1),W). [resolve(1533,a,126,c),unit_del(b,120)]. 1547 IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(1539,b,52,c)]. 1551 IsAFormOf(f1(f2(c1),c1),c1) | - IsTheFormOf(f2(c1),c1). [resolve(1547,c,1538,b),merge(c)]. 1552 IsAFormOf(f1(f2(c1),c1),c1). [resolve(1551,b,1533,a),merge(b)]. 1554 - Property(x) | Enc(f1(f2(c1),c1),x) | - Implies(c1,x). [resolve(1552,a,65,c),unit_del(a,603),unit_del(b,46)]. 1556 Ex1(A,f1(f2(c1),c1),W). [resolve(1552,a,60,c),unit_del(a,603),unit_del(b,46)]. 1573 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(1556,a,137,b),flip(d),unit_del(a,603)]. 1575 - Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | f1(f2(c1),c1) = f2(c1). [resolve(1556,a,135,b),flip(d),unit_del(a,603)]. 1681 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | IsTheFormOf(f2(c1),c1). [resolve(1573,c,63,e),unit_del(c,120),unit_del(d,46),unit_del(f,1529)]. 1708 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c2,f2(c1),W). [resolve(1681,c,127,c),unit_del(c,120)]. 1709 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | PartPTA(c3,f2(c1),W). [resolve(1681,c,126,c),unit_del(c,120)]. 1724 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1) | - PartPTA(c2,f2(c1),W). [resolve(1709,c,52,c)]. 1726 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))) | - IsTheFormOf(f2(c1),c1). [resolve(1724,d,1708,c),merge(d),merge(e)]. 1730 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(1726,c,1681,c),merge(c),merge(d)]. 1732 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | - Property(x) | - IsAFormOf(f1(f2(c1),c1),x) | Implies(x,f4(f2(c1),f1(f2(c1),c1))). [resolve(1730,b,64,e),unit_del(b,603),unit_del(e,764)]. 1733 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))) | Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(1732,c,1552,a),unit_del(b,46)]. 1741 Implies(c1,f4(f2(c1),f1(f2(c1),c1))). [resolve(1733,a,58,c),merge(d),unit_del(b,46),unit_del(c,764)]. 1745 Enc(f1(f2(c1),c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(1741,a,1554,c),unit_del(a,764)]. 1746 Enc(f2(c1),f4(f2(c1),f1(f2(c1),c1))). [resolve(1741,a,1532,c),unit_del(a,764)]. 1750 f1(f2(c1),c1) = f2(c1). [back_unit_del(1575),unit_del(a,1746),unit_del(b,1745)]. 1782 IsTheFormOf(f2(c1),c1). [resolve(1750,a,63,e),unit_del(a,120),unit_del(b,46),unit_del(d,1529)]. 1784 PartPTA(c2,f2(c1),W). [resolve(1782,a,127,c),unit_del(a,120)]. 1785 PartPTA(c3,f2(c1),W). [resolve(1782,a,126,c),unit_del(a,120)]. 1790 $F. [ur(52,a,1782,a,b,1784,a),unit_del(a,1785)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=740. Generated=3879. Kept=1744. proofs=1. Usable=186. Sos=88. Demods=1. Denials=0. Limbo=3, Disabled=1512. Hints=0. Megabytes=1.34. User_CPU=0.52, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3635 exit (max_proofs) Wed Jun 14 16:56:16 2006