============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3669 was started by zalta on mally, Wed Jun 14 16:56:37 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 = <196,77>. Problem reduction (0.00 sec) gives one subproblem (<383,69>); 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.06 (+ 0.01) seconds. % Length of proof is 54. % Level of proof is 17. % Maximum clause weight is 37. % Given clauses 108. 1 Form(c1). [clausify]. 3 - Form(x) | Object(x). [clausify]. 6 - Object(x) | - Form(x) | Property(f7(x)). [clausify]. 7 - Object(x) | - Form(x) | IsAFormOf(x,f7(x)). [clausify]. 21 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y). [clausify]. 22 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f5(x,y) != x. [clausify]. 23 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - IsTheFormOf(y,z) | - Enc(x,z). [clausify]. 31 - Object(c1) | Property(f7(c1)). [resolve(6,b,1,a)]. 32 - Object(c1) | IsAFormOf(c1,f7(c1)). [resolve(7,b,1,a)]. 40 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - Enc(x,z) | - Object(y) | - Property(z) | - IsAFormOf(y,z) | IsAFormOf(f5(y,z),z). [resolve(23,e,21,c)]. 41 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - Enc(x,z) | - Object(y) | - Property(z) | - IsAFormOf(y,z) | f5(y,z) != y. [resolve(23,e,22,c)]. 43 - PartPH(c1,c1). [clausify]. 44 - IsAFormOf(x,y) | Object(x). [clausify]. 46 - 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]. 52 - Property(x) | - Property(y) | Implies(x,y) | Ex1(x,f3(x,y),f4(x,y)). [clausify]. 53 - Property(x) | - Property(y) | Implies(x,y) | - Ex1(y,f3(x,y),f4(x,y)). [clausify]. 54 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f2(x,y)) | y = x. [clausify]. 57 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f2(x,y)) | Enc(y,f2(x,y)) | y = x. [clausify]. 58 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f2(x,y)) | - Enc(y,f2(x,y)) | y = x. [clausify]. 59 Object(c1). [resolve(3,a,1,a)]. 60 Property(f7(c1)). [copy(31),unit_del(a,59)]. 61 IsAFormOf(c1,f7(c1)). [copy(32),unit_del(a,59)]. 69 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - Enc(x,z) | - IsAFormOf(y,z) | IsAFormOf(f5(y,z),z). [copy(40),merge(f),merge(g)]. 70 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - Enc(x,z) | - IsAFormOf(y,z) | f5(y,z) != y. [copy(41),merge(f),merge(g)]. 75 - Object(x) | - Property(y) | - IsAFormOf(x,y) | Enc(x,y) | - Implies(y,y). [factor(50,b,d)]. 76 - Property(x) | Implies(x,x) | Ex1(x,f3(x,x),f4(x,x)). [factor(52,a,b)]. 77 - Property(x) | Implies(x,x) | - Ex1(x,f3(x,x),f4(x,x)). [factor(53,a,b)]. 82 - Object(x) | PartPH(x,x) | - Property(y) | - Enc(x,y) | - IsAFormOf(x,y) | IsAFormOf(f5(x,y),y). [factor(69,a,b)]. 83 - Object(x) | PartPH(x,x) | - Property(y) | - Enc(x,y) | - IsAFormOf(x,y) | f5(x,y) != x. [factor(70,a,b)]. 94 Ex1(A,c1,W). [resolve(61,a,46,c),unit_del(a,59),unit_del(b,60)]. 97 Implies(f7(c1),f7(c1)) | Ex1(f7(c1),f3(f7(c1),f7(c1)),f4(f7(c1),f7(c1))). [resolve(76,a,60,a)]. 98 - Object(x) | - Ex1(A,x,W) | - Enc(x,f2(x,c1)) | - Enc(c1,f2(x,c1)) | c1 = x. [resolve(94,a,58,d),unit_del(b,59)]. 100 - Object(x) | - Ex1(A,x,W) | Enc(x,f2(x,c1)) | Enc(c1,f2(x,c1)) | c1 = x. [resolve(94,a,57,d),unit_del(b,59)]. 104 - Object(x) | - Ex1(A,x,W) | Property(f2(x,c1)) | c1 = x. [resolve(94,a,54,d),unit_del(b,59)]. 108 Implies(f7(c1),f7(c1)). [resolve(97,b,77,c),merge(c),unit_del(b,60)]. 109 - Object(x) | - IsAFormOf(x,f7(c1)) | Enc(x,f7(c1)). [resolve(108,a,75,e),unit_del(b,60)]. 110 Enc(c1,f7(c1)). [resolve(109,b,61,a),unit_del(a,59)]. 111 IsAFormOf(f5(c1,f7(c1)),f7(c1)). [resolve(110,a,82,d),unit_del(a,59),unit_del(b,43),unit_del(c,60),unit_del(d,61)]. 114 f5(c1,f7(c1)) != c1. [ur(83,a,59,a,b,43,a,c,60,a,d,110,a,e,61,a)]. 120 - Object(f5(c1,f7(c1))) | Ex1(A,f5(c1,f7(c1)),W). [resolve(111,a,46,c),unit_del(b,60)]. 121 Object(f5(c1,f7(c1))). [resolve(111,a,44,a)]. 122 Ex1(A,f5(c1,f7(c1)),W). [back_unit_del(120),unit_del(a,121)]. 131 Property(f2(f5(c1,f7(c1)),c1)). [resolve(122,a,104,b),flip(c),unit_del(a,121),unit_del(c,114)]. 132 Enc(f5(c1,f7(c1)),f2(f5(c1,f7(c1)),c1)) | Enc(c1,f2(f5(c1,f7(c1)),c1)). [resolve(122,a,100,b),flip(d),unit_del(a,121),unit_del(d,114)]. 134 - Enc(f5(c1,f7(c1)),f2(f5(c1,f7(c1)),c1)) | - Enc(c1,f2(f5(c1,f7(c1)),c1)). [resolve(122,a,98,b),flip(d),unit_del(a,121),unit_del(d,114)]. 189 Enc(c1,f2(f5(c1,f7(c1)),c1)) | - Property(x) | - IsAFormOf(f5(c1,f7(c1)),x) | Implies(x,f2(f5(c1,f7(c1)),c1)). [resolve(132,a,49,e),unit_del(b,121),unit_del(e,131)]. 216 Enc(c1,f2(f5(c1,f7(c1)),c1)) | Implies(f7(c1),f2(f5(c1,f7(c1)),c1)). [resolve(189,c,111,a),unit_del(b,60)]. 217 Enc(c1,f2(f5(c1,f7(c1)),c1)) | - Object(x) | - IsAFormOf(x,f7(c1)) | Enc(x,f2(f5(c1,f7(c1)),c1)). [resolve(216,b,50,f),unit_del(c,60),unit_del(e,131)]. 218 Enc(c1,f2(f5(c1,f7(c1)),c1)). [factor(217,a,d),unit_del(b,59),unit_del(c,61)]. 219 - Enc(f5(c1,f7(c1)),f2(f5(c1,f7(c1)),c1)). [back_unit_del(134),unit_del(b,218)]. 222 - Implies(f7(c1),f2(f5(c1,f7(c1)),c1)). [ur(50,a,121,a,b,60,a,c,111,a,d,131,a,e,219,a)]. 226 $F. [ur(49,a,59,a,b,60,a,c,61,a,d,131,a,f,222,a),unit_del(a,218)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=108. Generated=301. Kept=183. proofs=1. Usable=102. Sos=54. Demods=0. Denials=0. Limbo=2, Disabled=67. Hints=0. Megabytes=0.33. User_CPU=0.06, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3669 exit (max_proofs) Wed Jun 14 16:56:37 2006