============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3625 was started by root on mally, Wed Jun 14 16:54:32 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 (4 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <115,57>. Problem reduction (0.00 sec) gives one subproblem (<256,47>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 18 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 18. % Level of proof is 5. % Maximum clause weight is 15. % Given clauses 32. 1 Object(c1). [clausify]. 5 - Object(x) | - Property(y) | - IsTheFormOf(x,y) | IsAFormOf(x,y). [clausify]. 12 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | Enc(x,z) | - Implies(y,z). [clausify]. 30 Property(c2). [clausify]. 31 IsTheFormOf(c1,c2). [clausify]. 32 - Enc(c1,c2). [clausify]. 33 - Property(x) | - Property(y) | Implies(x,y) | Ex1(x,f1(x,y),f2(x,y)). [clausify]. 34 - Property(x) | - Property(y) | Implies(x,y) | - Ex1(y,f1(x,y),f2(x,y)). [clausify]. 35 - Property(x) | - IsTheFormOf(c1,x) | IsAFormOf(c1,x). [resolve(5,a,1,a)]. 39 - Property(x) | - IsAFormOf(c1,x) | - Property(y) | Enc(c1,y) | - Implies(x,y). [resolve(12,a,1,a)]. 46 - Property(x) | Implies(x,x) | Ex1(x,f1(x,x),f2(x,x)). [factor(33,a,b)]. 47 - Property(x) | Implies(x,x) | - Ex1(x,f1(x,x),f2(x,x)). [factor(34,a,b)]. 49 - Property(x) | - IsAFormOf(c1,x) | Enc(c1,x) | - Implies(x,x). [factor(39,a,c)]. 60 IsAFormOf(c1,c2). [resolve(35,b,31,a),unit_del(a,30)]. 62 Implies(c2,c2) | Ex1(c2,f1(c2,c2),f2(c2,c2)). [resolve(46,a,30,a)]. 64 - Implies(c2,c2). [ur(49,a,30,a,b,60,a,c,32,a)]. 68 Ex1(c2,f1(c2,c2),f2(c2,c2)). [back_unit_del(62),unit_del(a,64)]. 69 $F. [ur(47,a,30,a,b,64,a),unit_del(a,68)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=32. Generated=60. Kept=39. proofs=1. Usable=28. Sos=6. Demods=0. Denials=0. Limbo=0, Disabled=34. Hints=0. Megabytes=0.09. User_CPU=0.01, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3625 exit (max_proofs) Wed Jun 14 16:54:32 2006