============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3670 was started by zalta on mally, Wed Jun 14 16:56:42 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 = <172,69>. Problem reduction (0.00 sec) gives one subproblem (<329,61>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 26 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.13 (+ 0.01) seconds. % Length of proof is 118. % Level of proof is 61. % Maximum clause weight is 120. % Given clauses 288. 1 Point(W). [clausify]. 3 - Object(x) | - Property(y) | - IsTheFormOf(x,y) | - PartPTA(x,x,W). [clausify]. 17 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f4(x,y),y). [clausify]. 18 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f4(x,y) != x. [clausify]. 21 - Object(x) | - Object(y) | - Point(z) | PartPTA(x,y,z) | - Property(u) | - IsTheFormOf(y,u) | - Ex1(u,x,z). [clausify]. 30 - Object(x) | - Object(y) | PartPTA(x,y,W) | - Property(z) | - IsTheFormOf(y,z) | - Ex1(z,x,W). [resolve(21,c,1,a)]. 31 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f4(x,y),y) | - Object(x) | - Property(y) | - PartPTA(x,x,W). [resolve(17,c,3,c)]. 33 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f4(x,y) != x | - Object(x) | - Property(y) | - PartPTA(x,x,W). [resolve(18,c,3,c)]. 38 - Object(x) | - Object(y) | PartPTA(x,y,W) | - Property(z) | - Ex1(z,x,W) | - Object(y) | - Property(z) | - IsAFormOf(y,z) | IsAFormOf(f4(y,z),z). [resolve(30,e,17,c)]. 39 - Object(x) | - Object(y) | PartPTA(x,y,W) | - Property(z) | - Ex1(z,x,W) | - Object(y) | - Property(z) | - IsAFormOf(y,z) | f4(y,z) != y. [resolve(30,e,18,c)]. 41 Property(A). [clausify]. 42 - IsAFormOf(x,y) | Object(x). [clausify]. 44 - Property(x) | Object(f2(x)). [clausify]. 45 - Property(x) | Ex1(A,f2(x),W). [clausify]. 46 - Property(x) | - Property(y) | - Enc(f2(x),y) | Implies(x,y). [clausify]. 47 - Property(x) | - Property(y) | Enc(f2(x),y) | - Implies(x,y). [clausify]. 48 - Object(x) | - Property(y) | - IsAFormOf(x,y) | Ex1(A,x,W). [clausify]. 49 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | - Enc(x,z) | Implies(y,z). [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) | - Ex1(A,x,W) | Property(f3(x,y)). [clausify]. 52 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f5(x,y)) | y = x. [clausify]. 53 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Enc(x,f3(x,y)) | Implies(y,f3(x,y)). [clausify]. 54 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | - Enc(x,f3(x,y)) | - Implies(y,f3(x,y)). [clausify]. 55 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f5(x,y)) | Enc(y,f5(x,y)) | y = x. [clausify]. 56 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f5(x,y)) | - Enc(y,f5(x,y)) | y = x. [clausify]. 59 - Object(x) | - Property(y) | - IsAFormOf(x,y) | IsAFormOf(f4(x,y),y) | - PartPTA(x,x,W). [copy(31),merge(e),merge(f)]. 61 - Object(x) | - Property(y) | - IsAFormOf(x,y) | f4(x,y) != x | - PartPTA(x,x,W). [copy(33),merge(e),merge(f)]. 66 - Object(x) | - Object(y) | PartPTA(x,y,W) | - Property(z) | - Ex1(z,x,W) | - IsAFormOf(y,z) | IsAFormOf(f4(y,z),z). [copy(38),merge(f),merge(g)]. 67 - Object(x) | - Object(y) | PartPTA(x,y,W) | - Property(z) | - Ex1(z,x,W) | - IsAFormOf(y,z) | f4(y,z) != y. [copy(39),merge(f),merge(g)]. 76 - Object(x) | PartPTA(x,x,W) | - Property(y) | - Ex1(y,x,W) | - IsAFormOf(x,y) | IsAFormOf(f4(x,y),y). [factor(66,a,b)]. 77 - Object(x) | PartPTA(x,x,W) | - Property(y) | - Ex1(y,x,W) | - IsAFormOf(x,y) | f4(x,y) != x. [factor(67,a,b)]. 79 Object(f2(A)). [resolve(44,a,41,a)]. 80 Ex1(A,f2(A),W). [resolve(45,a,41,a)]. 81 PartPTA(f2(A),f2(A),W) | - IsAFormOf(f2(A),A) | IsAFormOf(f4(f2(A),A),A). [resolve(80,a,76,d),unit_del(a,79),unit_del(c,41)]. 82 - Object(x) | PartPTA(f2(A),x,W) | - IsAFormOf(x,A) | IsAFormOf(f4(x,A),A). [resolve(80,a,66,e),unit_del(a,79),unit_del(d,41)]. 84 - Object(x) | - Ex1(A,x,W) | - Enc(f2(A),f5(f2(A),x)) | - Enc(x,f5(f2(A),x)) | f2(A) = x. [resolve(80,a,56,c),flip(f),unit_del(a,79)]. 86 - Object(x) | - Ex1(A,x,W) | Enc(f2(A),f5(f2(A),x)) | Enc(x,f5(f2(A),x)) | f2(A) = x. [resolve(80,a,55,c),flip(f),unit_del(a,79)]. 87 - Property(x) | IsAFormOf(f2(A),x) | - Enc(f2(A),f3(f2(A),x)) | - Implies(x,f3(f2(A),x)). [resolve(80,a,54,d),unit_del(a,79)]. 88 - Property(x) | IsAFormOf(f2(A),x) | Enc(f2(A),f3(f2(A),x)) | Implies(x,f3(f2(A),x)). [resolve(80,a,53,d),unit_del(a,79)]. 90 - Object(x) | - Ex1(A,x,W) | Property(f5(f2(A),x)) | f2(A) = x. [resolve(80,a,52,c),flip(e),unit_del(a,79)]. 91 - Property(x) | IsAFormOf(f2(A),x) | Property(f3(f2(A),x)). [resolve(80,a,51,d),unit_del(a,79)]. 92 IsAFormOf(f2(A),A) | Property(f3(f2(A),A)). [resolve(91,a,41,a)]. 93 Property(f3(f2(A),A)) | PartPTA(f2(A),f2(A),W) | IsAFormOf(f4(f2(A),A),A). [resolve(92,a,82,c),unit_del(b,79)]. 100 Property(f3(f2(A),A)) | IsAFormOf(f4(f2(A),A),A) | - Property(x) | - IsAFormOf(f2(A),x) | IsAFormOf(f4(f2(A),x),x). [resolve(93,b,59,e),unit_del(c,79)]. 101 Property(f3(f2(A),A)) | IsAFormOf(f4(f2(A),A),A) | - IsAFormOf(f2(A),A). [factor(100,b,e),unit_del(c,41)]. 102 Property(f3(f2(A),A)) | IsAFormOf(f4(f2(A),A),A). [resolve(101,c,92,a),merge(c)]. 107 Property(f3(f2(A),A)) | - Object(f4(f2(A),A)) | Ex1(A,f4(f2(A),A),W). [resolve(102,b,48,c),unit_del(c,41)]. 108 Property(f3(f2(A),A)) | Object(f4(f2(A),A)). [resolve(102,b,42,a)]. 113 IsAFormOf(f2(A),A) | Enc(f2(A),f3(f2(A),A)) | Implies(A,f3(f2(A),A)). [resolve(88,a,41,a)]. 115 IsAFormOf(f2(A),A) | Enc(f2(A),f3(f2(A),A)) | - Property(f3(f2(A),A)). [resolve(113,c,47,d),merge(e),unit_del(c,41)]. 116 IsAFormOf(f2(A),A) | Enc(f2(A),f3(f2(A),A)) | Object(f4(f2(A),A)). [resolve(115,c,108,a)]. 119 IsAFormOf(f2(A),A) | Object(f4(f2(A),A)) | - Property(f3(f2(A),A)) | Implies(A,f3(f2(A),A)). [resolve(116,b,46,c),unit_del(c,41)]. 120 IsAFormOf(f2(A),A) | Object(f4(f2(A),A)) | Implies(A,f3(f2(A),A)). [resolve(119,c,108,a),merge(d)]. 121 IsAFormOf(f2(A),A) | Object(f4(f2(A),A)) | - Enc(f2(A),f3(f2(A),A)). [resolve(120,c,87,d),merge(d),unit_del(c,41)]. 123 IsAFormOf(f2(A),A) | Object(f4(f2(A),A)). [resolve(121,c,116,b),merge(c),merge(d)]. 124 Object(f4(f2(A),A)) | PartPTA(f2(A),f2(A),W) | IsAFormOf(f4(f2(A),A),A). [resolve(123,a,82,c),unit_del(b,79)]. 131 Object(f4(f2(A),A)) | IsAFormOf(f4(f2(A),A),A) | - Property(x) | - IsAFormOf(f2(A),x) | IsAFormOf(f4(f2(A),x),x). [resolve(124,b,59,e),unit_del(c,79)]. 132 Object(f4(f2(A),A)) | IsAFormOf(f4(f2(A),A),A) | - IsAFormOf(f2(A),A). [factor(131,b,e),unit_del(c,41)]. 133 Object(f4(f2(A),A)) | IsAFormOf(f4(f2(A),A),A). [resolve(132,c,123,a),merge(c)]. 135 Object(f4(f2(A),A)). [resolve(133,b,42,a),merge(b)]. 136 Property(f3(f2(A),A)) | Ex1(A,f4(f2(A),A),W). [back_unit_del(107),unit_del(b,135)]. 140 Property(f3(f2(A),A)) | Property(f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(136,b,90,b),flip(d),unit_del(b,135)]. 142 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(136,b,86,b),flip(e),unit_del(b,135)]. 144 Property(f3(f2(A),A)) | - Enc(f2(A),f5(f2(A),f4(f2(A),A))) | - Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(136,b,84,b),flip(e),unit_del(b,135)]. 189 Property(f3(f2(A),A)) | Property(f5(f2(A),f4(f2(A),A))) | PartPTA(f2(A),f2(A),W) | - IsAFormOf(f2(A),A). [resolve(140,c,77,f),unit_del(c,79),unit_del(e,41),unit_del(f,80)]. 192 Property(f3(f2(A),A)) | Property(f5(f2(A),f4(f2(A),A))) | - IsAFormOf(f2(A),A) | - PartPTA(f2(A),f2(A),W). [resolve(140,c,61,d),unit_del(c,79),unit_del(d,41)]. 196 Property(f3(f2(A),A)) | Property(f5(f2(A),f4(f2(A),A))) | PartPTA(f2(A),f2(A),W). [resolve(189,d,92,a),merge(d)]. 206 Property(f3(f2(A),A)) | Property(f5(f2(A),f4(f2(A),A))) | - IsAFormOf(f2(A),A). [resolve(192,d,196,c),merge(d),merge(e)]. 207 Property(f3(f2(A),A)) | Property(f5(f2(A),f4(f2(A),A))). [resolve(206,c,92,a),merge(c)]. 214 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | PartPTA(f2(A),f2(A),W) | - IsAFormOf(f2(A),A). [resolve(142,d,77,f),unit_del(d,79),unit_del(f,41),unit_del(g,80)]. 217 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | - IsAFormOf(f2(A),A) | - PartPTA(f2(A),f2(A),W). [resolve(142,d,61,d),unit_del(d,79),unit_del(e,41)]. 329 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | PartPTA(f2(A),f2(A),W). [resolve(214,e,92,a),merge(e)]. 335 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | - IsAFormOf(f2(A),A). [resolve(217,e,329,d),merge(e),merge(f),merge(g)]. 336 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))). [resolve(335,d,92,a),merge(d)]. 339 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | - Property(x) | - IsAFormOf(f4(f2(A),A),x) | - Property(f5(f2(A),f4(f2(A),A))) | Implies(x,f5(f2(A),f4(f2(A),A))). [resolve(336,c,49,e),unit_del(c,135)]. 544 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | - Property(f5(f2(A),f4(f2(A),A))) | Implies(A,f5(f2(A),f4(f2(A),A))). [resolve(339,d,102,b),merge(f),unit_del(c,41)]. 545 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Implies(A,f5(f2(A),f4(f2(A),A))). [resolve(544,c,207,b),merge(d)]. 547 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))) | - Property(f5(f2(A),f4(f2(A),A))). [resolve(545,c,47,d),merge(e),unit_del(c,41)]. 548 Property(f3(f2(A),A)) | Enc(f2(A),f5(f2(A),f4(f2(A),A))). [resolve(547,c,207,b),merge(c)]. 551 Property(f3(f2(A),A)) | - Property(f5(f2(A),f4(f2(A),A))) | Implies(A,f5(f2(A),f4(f2(A),A))). [resolve(548,b,46,c),unit_del(b,41)]. 552 Property(f3(f2(A),A)) | Implies(A,f5(f2(A),f4(f2(A),A))). [resolve(551,b,207,b),merge(c)]. 553 Property(f3(f2(A),A)) | - Object(x) | - IsAFormOf(x,A) | - Property(f5(f2(A),f4(f2(A),A))) | Enc(x,f5(f2(A),f4(f2(A),A))). [resolve(552,b,50,f),unit_del(c,41)]. 555 Property(f3(f2(A),A)) | - Property(f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))). [resolve(553,c,102,b),merge(e),unit_del(b,135)]. 556 Property(f3(f2(A),A)) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))). [resolve(555,b,207,b),merge(c)]. 558 Property(f3(f2(A),A)) | - Enc(f2(A),f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(556,b,144,c),merge(b)]. 561 Property(f3(f2(A),A)) | f4(f2(A),A) = f2(A). [resolve(558,b,548,b),merge(c)]. 562 Property(f3(f2(A),A)) | PartPTA(f2(A),f2(A),W) | - IsAFormOf(f2(A),A). [resolve(561,b,77,f),unit_del(b,79),unit_del(d,41),unit_del(e,80)]. 565 Property(f3(f2(A),A)) | - IsAFormOf(f2(A),A) | - PartPTA(f2(A),f2(A),W). [resolve(561,b,61,d),unit_del(b,79),unit_del(c,41)]. 592 Property(f3(f2(A),A)) | PartPTA(f2(A),f2(A),W). [resolve(562,c,92,a),merge(c)]. 600 Property(f3(f2(A),A)) | - IsAFormOf(f2(A),A). [resolve(565,c,592,b),merge(c)]. 601 Property(f3(f2(A),A)). [resolve(600,b,92,a),merge(b)]. 604 IsAFormOf(f2(A),A) | Enc(f2(A),f3(f2(A),A)). [back_unit_del(115),unit_del(c,601)]. 616 IsAFormOf(f2(A),A) | Implies(A,f3(f2(A),A)). [resolve(604,b,46,c),unit_del(b,41),unit_del(c,601)]. 617 IsAFormOf(f2(A),A) | - Enc(f2(A),f3(f2(A),A)). [resolve(616,b,87,d),merge(c),unit_del(b,41)]. 619 IsAFormOf(f2(A),A). [resolve(617,b,604,b),merge(b)]. 624 PartPTA(f2(A),f2(A),W) | IsAFormOf(f4(f2(A),A),A). [back_unit_del(81),unit_del(b,619)]. 635 IsAFormOf(f4(f2(A),A),A) | - Property(x) | - IsAFormOf(f2(A),x) | IsAFormOf(f4(f2(A),x),x). [resolve(624,a,59,e),unit_del(b,79)]. 636 IsAFormOf(f4(f2(A),A),A). [factor(635,a,d),unit_del(b,41),unit_del(c,619)]. 641 Ex1(A,f4(f2(A),A),W). [resolve(636,a,48,c),unit_del(a,135),unit_del(b,41)]. 642 Property(f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(641,a,90,b),flip(c),unit_del(a,135)]. 644 Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(641,a,86,b),flip(d),unit_del(a,135)]. 646 - Enc(f2(A),f5(f2(A),f4(f2(A),A))) | - Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [resolve(641,a,84,b),flip(d),unit_del(a,135)]. 697 Property(f5(f2(A),f4(f2(A),A))) | PartPTA(f2(A),f2(A),W). [resolve(642,b,77,f),unit_del(b,79),unit_del(d,41),unit_del(e,80),unit_del(f,619)]. 700 Property(f5(f2(A),f4(f2(A),A))) | - PartPTA(f2(A),f2(A),W). [resolve(642,b,61,d),unit_del(b,79),unit_del(c,41),unit_del(d,619)]. 706 Property(f5(f2(A),f4(f2(A),A))). [resolve(700,b,697,b),merge(b)]. 726 Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | PartPTA(f2(A),f2(A),W). [resolve(644,c,77,f),unit_del(c,79),unit_del(e,41),unit_del(f,80),unit_del(g,619)]. 729 Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | - PartPTA(f2(A),f2(A),W). [resolve(644,c,61,d),unit_del(c,79),unit_del(d,41),unit_del(e,619)]. 768 Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))). [resolve(729,c,726,c),merge(c),merge(d)]. 770 Enc(f2(A),f5(f2(A),f4(f2(A),A))) | - Property(x) | - IsAFormOf(f4(f2(A),A),x) | Implies(x,f5(f2(A),f4(f2(A),A))). [resolve(768,b,49,e),unit_del(b,135),unit_del(e,706)]. 773 Enc(f2(A),f5(f2(A),f4(f2(A),A))) | Implies(A,f5(f2(A),f4(f2(A),A))). [resolve(770,c,636,a),unit_del(b,41)]. 775 Enc(f2(A),f5(f2(A),f4(f2(A),A))). [resolve(773,b,47,d),merge(d),unit_del(b,41),unit_del(c,706)]. 776 - Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))) | f4(f2(A),A) = f2(A). [back_unit_del(646),unit_del(a,775)]. 779 Implies(A,f5(f2(A),f4(f2(A),A))). [resolve(775,a,46,c),unit_del(a,41),unit_del(b,706)]. 781 - Object(x) | - IsAFormOf(x,A) | Enc(x,f5(f2(A),f4(f2(A),A))). [resolve(779,a,50,f),unit_del(b,41),unit_del(d,706)]. 786 Enc(f4(f2(A),A),f5(f2(A),f4(f2(A),A))). [resolve(781,b,636,a),unit_del(a,135)]. 787 f4(f2(A),A) = f2(A). [back_unit_del(776),unit_del(a,786)]. 797 PartPTA(f2(A),f2(A),W). [resolve(787,a,77,f),unit_del(a,79),unit_del(c,41),unit_del(d,80),unit_del(e,619)]. 800 $F. [resolve(787,a,61,d),unit_del(a,79),unit_del(b,41),unit_del(c,619),unit_del(d,797)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=288. Generated=1951. Kept=759. proofs=1. Usable=60. Sos=20. Demods=1. Denials=0. Limbo=3, Disabled=716. Hints=0. Megabytes=0.53. User_CPU=0.13, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3670 exit (max_proofs) Wed Jun 14 16:56:42 2006