============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3623 was started by root on mally, Wed Jun 14 16:53:36 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 (3 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <75,44>. Problem reduction (0.00 sec) gives one subproblem (<159,36>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 12 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.01 (+ 0.02) seconds. % Length of proof is 28. % Level of proof is 7. % Maximum clause weight is 37. % Given clauses 24. 2 - Object(x) | - IsAFormOf(x,c1). [clausify]. 3 - Property(x) | Object(f2(x)). [clausify]. 4 - Property(x) | Ex1(A,f2(x),W). [clausify]. 6 - Property(x) | - Property(y) | - Enc(f2(x),y) | Implies(x,y). [clausify]. 7 - Property(x) | - Property(y) | Enc(f2(x),y) | - Implies(x,y). [clausify]. 10 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Property(f1(x,y)). [clausify]. 11 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | Enc(x,f1(x,y)) | Implies(y,f1(x,y)). [clausify]. 12 - Object(x) | - Property(y) | IsAFormOf(x,y) | - Ex1(A,x,W) | - Enc(x,f1(x,y)) | - Implies(y,f1(x,y)). [clausify]. 17 - Property(x) | IsAFormOf(f2(y),x) | - Ex1(A,f2(y),W) | Property(f1(f2(y),x)) | - Property(y). [resolve(10,a,3,b)]. 18 - Property(x) | IsAFormOf(f2(y),x) | - Ex1(A,f2(y),W) | Enc(f2(y),f1(f2(y),x)) | Implies(x,f1(f2(y),x)) | - Property(y). [resolve(11,a,3,b)]. 19 - Property(x) | IsAFormOf(f2(y),x) | - Ex1(A,f2(y),W) | - Enc(f2(y),f1(f2(y),x)) | - Implies(x,f1(f2(y),x)) | - Property(y). [resolve(12,a,3,b)]. 20 - Property(x) | IsAFormOf(f2(y),x) | Property(f1(f2(y),x)) | - Property(y) | - Property(y). [resolve(17,c,4,b)]. 22 - Property(x) | IsAFormOf(f2(y),x) | Enc(f2(y),f1(f2(y),x)) | Implies(x,f1(f2(y),x)) | - Property(y) | - Property(y). [resolve(18,c,4,b)]. 24 - Property(x) | IsAFormOf(f2(y),x) | - Enc(f2(y),f1(f2(y),x)) | - Implies(x,f1(f2(y),x)) | - Property(y) | - Property(y). [resolve(19,c,4,b)]. 29 - Property(x) | IsAFormOf(f2(y),x) | Implies(x,f1(f2(y),x)) | - Property(y) | - Property(y) | - Property(y) | - Property(f1(f2(y),x)) | Implies(y,f1(f2(y),x)). [resolve(22,c,6,c)]. 31 - Property(x) | IsAFormOf(f2(y),x) | - Implies(x,f1(f2(y),x)) | - Property(y) | - Property(y) | - Property(y) | - Property(f1(f2(y),x)) | - Implies(y,f1(f2(y),x)). [resolve(24,c,7,c)]. 33 Property(c1). [clausify]. 34 - Property(x) | - IsAFormOf(f2(x),c1). [resolve(3,b,2,a)]. 35 - Property(x) | IsAFormOf(f2(y),x) | Property(f1(f2(y),x)) | - Property(y). [copy(20),merge(e)]. 39 - Property(x) | IsAFormOf(f2(y),x) | Implies(x,f1(f2(y),x)) | - Property(y) | - Property(f1(f2(y),x)) | Implies(y,f1(f2(y),x)). [copy(29),merge(e),merge(f)]. 41 - Property(x) | IsAFormOf(f2(y),x) | - Implies(x,f1(f2(y),x)) | - Property(y) | - Property(f1(f2(y),x)) | - Implies(y,f1(f2(y),x)). [copy(31),merge(e),merge(f)]. 43 - Property(x) | IsAFormOf(f2(x),x) | Property(f1(f2(x),x)). [factor(35,a,d)]. 51 - Property(x) | IsAFormOf(f2(x),x) | Implies(x,f1(f2(x),x)) | - Property(f1(f2(x),x)). [factor(39,a,d),merge(e)]. 53 - Property(x) | IsAFormOf(f2(x),x) | - Implies(x,f1(f2(x),x)) | - Property(f1(f2(x),x)). [factor(41,a,d),merge(e)]. 55 - IsAFormOf(f2(c1),c1). [ur(34,a,33,a)]. 58 Property(f1(f2(c1),c1)). [resolve(43,a,33,a),unit_del(a,55)]. 59 Implies(c1,f1(f2(c1),c1)). [resolve(58,a,51,d),unit_del(a,33),unit_del(b,55)]. 63 $F. [ur(53,a,33,a,b,55,a,d,58,a),unit_del(a,59)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=24. Generated=66. Kept=30. proofs=1. Usable=24. Sos=2. Demods=0. Denials=0. Limbo=4, Disabled=29. Hints=0. Megabytes=0.07. User_CPU=0.01, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3623 exit (max_proofs) Wed Jun 14 16:53:36 2006