============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3668 was started by zalta on mally, Wed Jun 14 16:56:31 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 = <199,76>. Problem reduction (0.00 sec) gives one subproblem (<373,67>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 29 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.19 (+ 0.01) seconds. % Length of proof is 124. % Level of proof is 62. % Maximum clause weight is 120. % Given clauses 369. 2 - Object(x) | - Property(y) | - IsTheFormOf(x,y) | - PartPH(x,x). [clausify]. 21 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - IsTheFormOf(y,z) | - Enc(x,z). [clausify]. 22 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y). [clausify]. 23 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f5(x,y) != x. [clausify]. 34 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y) | - Object(x) | - Property(y) | - PartPH(x,x). [resolve(22,c,2,c)]. 36 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y) | - Object(z) | - Object(x) | PartPH(z,x) | - Property(y) | - Enc(z,y). [resolve(22,c,21,e)]. 37 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f5(x,y) != x | - Object(x) | - Property(y) | - PartPH(x,x). [resolve(23,c,2,c)]. 39 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f5(x,y) != x | - Object(z) | - Object(x) | PartPH(z,x) | - Property(y) | - Enc(z,y). [resolve(23,c,21,e)]. 41 Property(A). [clausify]. 42 - IsAFormOf(x,y) | Object(x). [clausify]. 44 - Property(x) | Object(f6(x)). [clausify]. 45 - Property(x) | Ex1(A,f6(x),W). [clausify]. 46 - Object(x) | - Property(y) | - IsAFormOf(x,y) | Ex1(A,x,W). [clausify]. 48 - Property(x) | - Property(y) | - Enc(f6(x),y) | Implies(x,y). [clausify]. 49 - Property(x) | - Property(y) | Enc(f6(x),y) | - Implies(x,y). [clausify]. 51 - Property(x) | - Property(y) | Implies(x,y) | Ex1(x,f1(x,y),f2(x,y)). [clausify]. 52 - Property(x) | - Property(y) | Implies(x,y) | - Ex1(y,f1(x,y),f2(x,y)). [clausify]. 53 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | - Enc(x,z) | Implies(y,z). [clausify]. 54 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | Enc(x,z) | - Implies(y,z). [clausify]. 55 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Property(f3(x,y)). [clausify]. 56 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | y = x. [clausify]. 57 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Enc(x,f3(x,y)) | Implies(y,f3(x,y)). [clausify]. 58 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | - Enc(x,f3(x,y)) | - Implies(y,f3(x,y)). [clausify]. 59 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Enc(y,f7(x,y)) | y = x. [clausify]. 60 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f7(x,y)) | - Enc(y,f7(x,y)) | y = x. [clausify]. 65 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y) | - PartPH(x,x). [copy(34),merge(e),merge(f)]. 67 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y) | - Object(z) | PartPH(z,x) | - Enc(z,y). [copy(36),merge(f),merge(h)]. 68 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f5(x,y) != x | - PartPH(x,x). [copy(37),merge(e),merge(f)]. 70 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f5(x,y) != x | - Object(z) | PartPH(z,x) | - Enc(z,y). [copy(39),merge(f),merge(h)]. 74 - Property(x) | Enc(f6(x),x) | - Implies(x,x). [factor(49,a,b)]. 76 - Property(x) | Implies(x,x) | Ex1(x,f1(x,x),f2(x,x)). [factor(51,a,b)]. 77 - Property(x) | Implies(x,x) | - Ex1(x,f1(x,x),f2(x,x)). [factor(52,a,b)]. 82 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y) | PartPH(x,x) | - Enc(x,y). [factor(67,a,e)]. 83 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f5(x,y) != x | PartPH(x,x) | - Enc(x,y). [factor(70,a,e)]. 92 Object(f6(A)). [resolve(44,a,41,a)]. 93 Ex1(A,f6(A),W). [resolve(45,a,41,a)]. 96 Implies(A,A) | Ex1(A,f1(A,A),f2(A,A)). [resolve(76,a,41,a)]. 98 - Object(x) | - Ex1(A,x,W) | - Enc(f6(A),f7(f6(A),x)) | - Enc(x,f7(f6(A),x)) | f6(A) = x. [resolve(93,a,60,c),flip(f),unit_del(a,92)]. 100 - Object(x) | - Ex1(A,x,W) | Enc(f6(A),f7(f6(A),x)) | Enc(x,f7(f6(A),x)) | f6(A) = x. [resolve(93,a,59,c),flip(f),unit_del(a,92)]. 101 - Property(x) | IsAFormOf(f6(A),x) | - Enc(f6(A),f3(f6(A),x)) | - Implies(x,f3(f6(A),x)). [resolve(93,a,58,d),unit_del(a,92)]. 102 - Property(x) | IsAFormOf(f6(A),x) | Enc(f6(A),f3(f6(A),x)) | Implies(x,f3(f6(A),x)). [resolve(93,a,57,d),unit_del(a,92)]. 104 - Object(x) | - Ex1(A,x,W) | Property(f7(f6(A),x)) | f6(A) = x. [resolve(93,a,56,c),flip(e),unit_del(a,92)]. 105 - Property(x) | IsAFormOf(f6(A),x) | Property(f3(f6(A),x)). [resolve(93,a,55,d),unit_del(a,92)]. 107 Implies(A,A). [resolve(96,b,77,c),merge(c),unit_del(b,41)]. 109 Enc(f6(A),A). [resolve(107,a,74,c),unit_del(a,41)]. 110 - IsAFormOf(f6(A),A) | IsAFormOf(f5(f6(A),A),A) | PartPH(f6(A),f6(A)). [resolve(109,a,82,f),unit_del(a,92),unit_del(b,41)]. 111 - Object(x) | - IsAFormOf(x,A) | IsAFormOf(f5(x,A),A) | PartPH(f6(A),x). [resolve(109,a,67,g),unit_del(b,41),unit_del(e,92)]. 113 IsAFormOf(f6(A),A) | Property(f3(f6(A),A)). [resolve(105,a,41,a)]. 114 Property(f3(f6(A),A)) | IsAFormOf(f5(f6(A),A),A) | PartPH(f6(A),f6(A)). [resolve(113,a,111,b),unit_del(b,92)]. 120 Property(f3(f6(A),A)) | IsAFormOf(f5(f6(A),A),A) | - Property(x) | - IsAFormOf(f6(A),x) | IsAFormOf(f5(f6(A),x),x). [resolve(114,c,65,e),unit_del(c,92)]. 122 Property(f3(f6(A),A)) | IsAFormOf(f5(f6(A),A),A) | - IsAFormOf(f6(A),A). [factor(120,b,e),unit_del(c,41)]. 123 Property(f3(f6(A),A)) | IsAFormOf(f5(f6(A),A),A). [resolve(122,c,113,a),merge(c)]. 129 Property(f3(f6(A),A)) | - Object(f5(f6(A),A)) | Ex1(A,f5(f6(A),A),W). [resolve(123,b,46,c),unit_del(c,41)]. 130 Property(f3(f6(A),A)) | Object(f5(f6(A),A)). [resolve(123,b,42,a)]. 140 IsAFormOf(f6(A),A) | Enc(f6(A),f3(f6(A),A)) | Implies(A,f3(f6(A),A)). [resolve(102,a,41,a)]. 142 IsAFormOf(f6(A),A) | Enc(f6(A),f3(f6(A),A)) | - Property(f3(f6(A),A)). [resolve(140,c,49,d),merge(e),unit_del(c,41)]. 143 IsAFormOf(f6(A),A) | Enc(f6(A),f3(f6(A),A)) | Object(f5(f6(A),A)). [resolve(142,c,130,a)]. 148 IsAFormOf(f6(A),A) | Object(f5(f6(A),A)) | - Property(f3(f6(A),A)) | Implies(A,f3(f6(A),A)). [resolve(143,b,48,c),unit_del(c,41)]. 149 IsAFormOf(f6(A),A) | Object(f5(f6(A),A)) | Implies(A,f3(f6(A),A)). [resolve(148,c,130,a),merge(d)]. 150 IsAFormOf(f6(A),A) | Object(f5(f6(A),A)) | - Enc(f6(A),f3(f6(A),A)). [resolve(149,c,101,d),merge(d),unit_del(c,41)]. 152 IsAFormOf(f6(A),A) | Object(f5(f6(A),A)). [resolve(150,c,143,b),merge(c),merge(d)]. 153 Object(f5(f6(A),A)) | IsAFormOf(f5(f6(A),A),A) | PartPH(f6(A),f6(A)). [resolve(152,a,111,b),unit_del(b,92)]. 159 Object(f5(f6(A),A)) | IsAFormOf(f5(f6(A),A),A) | - Property(x) | - IsAFormOf(f6(A),x) | IsAFormOf(f5(f6(A),x),x). [resolve(153,c,65,e),unit_del(c,92)]. 161 Object(f5(f6(A),A)) | IsAFormOf(f5(f6(A),A),A) | - IsAFormOf(f6(A),A). [factor(159,b,e),unit_del(c,41)]. 162 Object(f5(f6(A),A)) | IsAFormOf(f5(f6(A),A),A). [resolve(161,c,152,a),merge(c)]. 164 Object(f5(f6(A),A)). [resolve(162,b,42,a),merge(b)]. 165 Property(f3(f6(A),A)) | Ex1(A,f5(f6(A),A),W). [back_unit_del(129),unit_del(b,164)]. 170 Property(f3(f6(A),A)) | Property(f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(165,b,104,b),flip(d),unit_del(b,164)]. 172 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(165,b,100,b),flip(e),unit_del(b,164)]. 174 Property(f3(f6(A),A)) | - Enc(f6(A),f7(f6(A),f5(f6(A),A))) | - Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(165,b,98,b),flip(e),unit_del(b,164)]. 206 Property(f3(f6(A),A)) | Property(f7(f6(A),f5(f6(A),A))) | - IsAFormOf(f6(A),A) | PartPH(f6(A),f6(A)). [resolve(170,c,83,d),unit_del(c,92),unit_del(d,41),unit_del(g,109)]. 209 Property(f3(f6(A),A)) | Property(f7(f6(A),f5(f6(A),A))) | - IsAFormOf(f6(A),A) | - PartPH(f6(A),f6(A)). [resolve(170,c,68,d),unit_del(c,92),unit_del(d,41)]. 239 Property(f3(f6(A),A)) | Property(f7(f6(A),f5(f6(A),A))) | PartPH(f6(A),f6(A)). [resolve(206,c,113,a),merge(d)]. 245 Property(f3(f6(A),A)) | Property(f7(f6(A),f5(f6(A),A))) | - IsAFormOf(f6(A),A). [resolve(209,d,239,c),merge(d),merge(e)]. 246 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | - IsAFormOf(f6(A),A) | PartPH(f6(A),f6(A)). [resolve(172,d,83,d),unit_del(d,92),unit_del(e,41),unit_del(h,109)]. 249 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | - IsAFormOf(f6(A),A) | - PartPH(f6(A),f6(A)). [resolve(172,d,68,d),unit_del(d,92),unit_del(e,41)]. 250 Property(f3(f6(A),A)) | Property(f7(f6(A),f5(f6(A),A))). [resolve(245,c,113,a),merge(c)]. 373 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | PartPH(f6(A),f6(A)). [resolve(246,d,113,a),merge(e)]. 381 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | - IsAFormOf(f6(A),A). [resolve(249,e,373,d),merge(e),merge(f),merge(g)]. 382 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))). [resolve(381,d,113,a),merge(d)]. 384 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | - Property(x) | - IsAFormOf(f5(f6(A),A),x) | - Property(f7(f6(A),f5(f6(A),A))) | Implies(x,f7(f6(A),f5(f6(A),A))). [resolve(382,c,53,e),unit_del(c,164)]. 627 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | - Property(f7(f6(A),f5(f6(A),A))) | Implies(A,f7(f6(A),f5(f6(A),A))). [resolve(384,d,123,b),merge(f),unit_del(c,41)]. 628 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Implies(A,f7(f6(A),f5(f6(A),A))). [resolve(627,c,250,b),merge(d)]. 631 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))) | - Property(f7(f6(A),f5(f6(A),A))). [resolve(628,c,49,d),merge(e),unit_del(c,41)]. 632 Property(f3(f6(A),A)) | Enc(f6(A),f7(f6(A),f5(f6(A),A))). [resolve(631,c,250,b),merge(c)]. 635 Property(f3(f6(A),A)) | - Property(f7(f6(A),f5(f6(A),A))) | Implies(A,f7(f6(A),f5(f6(A),A))). [resolve(632,b,48,c),unit_del(b,41)]. 636 Property(f3(f6(A),A)) | Implies(A,f7(f6(A),f5(f6(A),A))). [resolve(635,b,250,b),merge(c)]. 637 Property(f3(f6(A),A)) | - Object(x) | - IsAFormOf(x,A) | - Property(f7(f6(A),f5(f6(A),A))) | Enc(x,f7(f6(A),f5(f6(A),A))). [resolve(636,b,54,f),unit_del(c,41)]. 639 Property(f3(f6(A),A)) | - Property(f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))). [resolve(637,c,123,b),merge(e),unit_del(b,164)]. 640 Property(f3(f6(A),A)) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))). [resolve(639,b,250,b),merge(c)]. 642 Property(f3(f6(A),A)) | - Enc(f6(A),f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(640,b,174,c),merge(b)]. 645 Property(f3(f6(A),A)) | f5(f6(A),A) = f6(A). [resolve(642,b,632,b),merge(c)]. 646 Property(f3(f6(A),A)) | - IsAFormOf(f6(A),A) | PartPH(f6(A),f6(A)). [resolve(645,b,83,d),unit_del(b,92),unit_del(c,41),unit_del(f,109)]. 649 Property(f3(f6(A),A)) | - IsAFormOf(f6(A),A) | - PartPH(f6(A),f6(A)). [resolve(645,b,68,d),unit_del(b,92),unit_del(c,41)]. 676 Property(f3(f6(A),A)) | PartPH(f6(A),f6(A)). [resolve(646,b,113,a),merge(c)]. 683 Property(f3(f6(A),A)) | - IsAFormOf(f6(A),A). [resolve(649,c,676,b),merge(c)]. 684 Property(f3(f6(A),A)). [resolve(683,b,113,a),merge(b)]. 685 IsAFormOf(f6(A),A) | Enc(f6(A),f3(f6(A),A)). [back_unit_del(142),unit_del(c,684)]. 703 IsAFormOf(f6(A),A) | Implies(A,f3(f6(A),A)). [resolve(685,b,48,c),unit_del(b,41),unit_del(c,684)]. 704 IsAFormOf(f6(A),A) | - Enc(f6(A),f3(f6(A),A)). [resolve(703,b,101,d),merge(c),unit_del(b,41)]. 706 IsAFormOf(f6(A),A). [resolve(704,b,685,b),merge(b)]. 711 IsAFormOf(f5(f6(A),A),A) | PartPH(f6(A),f6(A)). [back_unit_del(110),unit_del(a,706)]. 722 IsAFormOf(f5(f6(A),A),A) | - Property(x) | - IsAFormOf(f6(A),x) | IsAFormOf(f5(f6(A),x),x). [resolve(711,b,65,e),unit_del(b,92)]. 724 IsAFormOf(f5(f6(A),A),A). [factor(722,a,d),unit_del(b,41),unit_del(c,706)]. 730 Ex1(A,f5(f6(A),A),W). [resolve(724,a,46,c),unit_del(a,164),unit_del(b,41)]. 738 Property(f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(730,a,104,b),flip(c),unit_del(a,164)]. 740 Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(730,a,100,b),flip(d),unit_del(a,164)]. 742 - Enc(f6(A),f7(f6(A),f5(f6(A),A))) | - Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [resolve(730,a,98,b),flip(d),unit_del(a,164)]. 792 Property(f7(f6(A),f5(f6(A),A))) | PartPH(f6(A),f6(A)). [resolve(738,b,83,d),unit_del(b,92),unit_del(c,41),unit_del(d,706),unit_del(f,109)]. 795 Property(f7(f6(A),f5(f6(A),A))) | - PartPH(f6(A),f6(A)). [resolve(738,b,68,d),unit_del(b,92),unit_del(c,41),unit_del(d,706)]. 801 Property(f7(f6(A),f5(f6(A),A))). [resolve(795,b,792,b),merge(b)]. 839 Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | PartPH(f6(A),f6(A)). [resolve(740,c,83,d),unit_del(c,92),unit_del(d,41),unit_del(e,706),unit_del(g,109)]. 842 Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | - PartPH(f6(A),f6(A)). [resolve(740,c,68,d),unit_del(c,92),unit_del(d,41),unit_del(e,706)]. 913 Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))). [resolve(842,c,839,c),merge(c),merge(d)]. 915 Enc(f6(A),f7(f6(A),f5(f6(A),A))) | - Property(x) | - IsAFormOf(f5(f6(A),A),x) | Implies(x,f7(f6(A),f5(f6(A),A))). [resolve(913,b,53,e),unit_del(b,164),unit_del(e,801)]. 927 Enc(f6(A),f7(f6(A),f5(f6(A),A))) | Implies(A,f7(f6(A),f5(f6(A),A))). [resolve(915,c,724,a),unit_del(b,41)]. 930 Enc(f6(A),f7(f6(A),f5(f6(A),A))). [resolve(927,b,49,d),merge(d),unit_del(b,41),unit_del(c,801)]. 931 - Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))) | f5(f6(A),A) = f6(A). [back_unit_del(742),unit_del(a,930)]. 936 Implies(A,f7(f6(A),f5(f6(A),A))). [resolve(930,a,48,c),unit_del(a,41),unit_del(b,801)]. 941 - Object(x) | - IsAFormOf(x,A) | Enc(x,f7(f6(A),f5(f6(A),A))). [resolve(936,a,54,f),unit_del(b,41),unit_del(d,801)]. 943 Enc(f5(f6(A),A),f7(f6(A),f5(f6(A),A))). [resolve(941,b,724,a),unit_del(a,164)]. 944 f5(f6(A),A) = f6(A). [back_unit_del(931),unit_del(a,943)]. 957 PartPH(f6(A),f6(A)). [resolve(944,a,83,d),unit_del(a,92),unit_del(b,41),unit_del(c,706),unit_del(e,109)]. 960 $F. [resolve(944,a,68,d),unit_del(a,92),unit_del(b,41),unit_del(c,706),unit_del(d,957)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=369. Generated=2418. Kept=919. proofs=1. Usable=100. Sos=27. Demods=1. Denials=0. Limbo=3, Disabled=829. Hints=0. Megabytes=0.61. User_CPU=0.19, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3668 exit (max_proofs) Wed Jun 14 16:56:31 2006