============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3631 was started by root on mally, Wed Jun 14 16:55:48 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 (6 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <155,70>. Problem reduction (0.00 sec) gives 2 independent subproblems: ( ). Max nnf_size of subproblems is 325; max cnf_max is 57. ============================== FOF REDUCTION MULTISEARCH ============= Starting Subproblem 1 of 2. Child search process 3632 started. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 57 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.00) seconds. % Length of proof is 9. % Level of proof is 1. % Maximum clause weight is 19. % Given clauses 26. 58 Point(W). [clausify]. 59 Object(c1). [clausify]. 60 Object(c2). [clausify]. 61 Property(c3). [clausify]. 62 IsTheFormOf(c1,c3). [clausify]. 63 Ex1(c3,c2,W). [clausify]. 64 - PartPTA(c2,c1,W). [clausify]. 83 - Object(x) | - Object(y) | - Point(z) | PartPTA(x,y,z) | - Property(u) | - IsTheFormOf(y,u) | - Ex1(u,x,z). [clausify]. 160 $F. [ur(83,b,59,a,c,58,a,d,64,a,e,61,a,f,62,a,g,63,a),unit_del(a,60)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=26. Generated=117. Kept=102. proofs=1. Usable=26. Sos=75. Demods=0. Denials=0. Limbo=1, Disabled=57. Hints=0. Megabytes=0.28. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3632 exit (max_proofs) Wed Jun 14 16:55:48 2006 ============================== continuing FOF reduction multisearch == Starting Subproblem 2 of 2. Child search process 3633 started. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 57 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.03 (+ 0.00) seconds. % Length of proof is 34. % Level of proof is 7. % Maximum clause weight is 17. % Given clauses 103. 6 PartPTA(c2,c1,W). [clausify]. 16 - Object(x) | - Object(y) | - Point(z) | Property(f11(x,y,z)) | - PartPTA(x,y,z). [clausify]. 19 - Object(x) | - Object(y) | - Point(z) | IsTheFormOf(y,f11(x,y,z)) | - PartPTA(x,y,z). [clausify]. 21 - Object(x) | - Object(y) | - Point(z) | Ex1(f11(x,y,z),x,z) | - PartPTA(x,y,z). [clausify]. 58 - Object(c2) | - Object(c1) | - Point(W) | Property(f11(c2,c1,W)). [resolve(16,e,6,a)]. 59 - Object(c2) | - Object(c1) | - Point(W) | IsTheFormOf(c1,f11(c2,c1,W)). [resolve(19,e,6,a)]. 60 - Object(c2) | - Object(c1) | - Point(W) | Ex1(f11(c2,c1,W),c2,W). [resolve(21,e,6,a)]. 64 Point(W). [clausify]. 65 Object(c1). [clausify]. 66 Object(c2). [clausify]. 67 Property(c3). [clausify]. 68 IsTheFormOf(c1,c3). [clausify]. 69 - Ex1(c3,c2,W). [clausify]. 70 - Object(x) | - Property(y) | IsAFormOf(x,y) | - IsTheFormOf(x,y). [clausify]. 74 - Property(x) | - Property(y) | Implies(x,y) | Ex1(x,f1(x,y),f2(x,y)). [clausify]. 75 - Property(x) | - Property(y) | Implies(x,y) | - Ex1(y,f1(x,y),f2(x,y)). [clausify]. 76 - Object(x) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - IsAFormOf(x,y). [clausify]. 77 - Object(x) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - IsAFormOf(x,y). [clausify]. 80 - Property(x) | - Property(y) | - Point(z) | - Ex1(x,u,z) | Ex1(y,u,z) | - Implies(x,y). [clausify]. 116 Property(f11(c2,c1,W)). [copy(58),unit_del(a,66),unit_del(b,65),unit_del(c,64)]. 117 IsTheFormOf(c1,f11(c2,c1,W)). [copy(59),unit_del(a,66),unit_del(b,65),unit_del(c,64)]. 118 Ex1(f11(c2,c1,W),c2,W). [copy(60),unit_del(a,66),unit_del(b,65),unit_del(c,64)]. 123 - Property(x) | Implies(x,x) | Ex1(x,f1(x,x),f2(x,x)). [factor(74,a,b)]. 124 - Property(x) | Implies(x,x) | - Ex1(x,f1(x,x),f2(x,x)). [factor(75,a,b)]. 125 - Object(x) | - Property(y) | Enc(x,y) | - Implies(y,y) | - IsAFormOf(x,y). [factor(76,b,c)]. 157 IsAFormOf(c1,c3). [resolve(70,d,68,a),unit_del(a,65),unit_del(b,67)]. 168 IsAFormOf(c1,f11(c2,c1,W)). [resolve(117,a,70,d),unit_del(a,65),unit_del(b,116)]. 177 - Implies(f11(c2,c1,W),c3). [ur(80,a,116,a,b,67,a,c,64,a,d,118,a,e,69,a)]. 184 Implies(c3,c3) | Ex1(c3,f1(c3,c3),f2(c3,c3)). [resolve(123,a,67,a)]. 192 Enc(c1,c3) | - Implies(c3,c3). [resolve(157,a,125,e),unit_del(a,65),unit_del(b,67)]. 202 - Enc(c1,c3). [ur(77,a,65,a,b,116,a,c,67,a,d,177,a,f,168,a)]. 203 - Implies(c3,c3). [back_unit_del(192),unit_del(a,202)]. 204 Ex1(c3,f1(c3,c3),f2(c3,c3)). [back_unit_del(184),unit_del(a,203)]. 207 $F. [ur(124,a,67,a,b,203,a),unit_del(a,204)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=103. Generated=171. Kept=143. proofs=1. Usable=101. Sos=38. Demods=0. Denials=0. Limbo=0, Disabled=67. Hints=0. Megabytes=0.35. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3633 exit (max_proofs) Wed Jun 14 16:55:48 2006 ============================== end of multisearch ==================== All 2 subproblems have been proved, so we are done. Total user_CPU=0.05, system_CPU=0.02, wall_clock=0. THEOREM PROVED Exiting. Process 3631 exit (max_proofs) Wed Jun 14 16:55:48 2006