============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3671 was started by zalta on mally, Wed Jun 14 16:56:49 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 = <80,21>. Problem reduction (0.00 sec) gives one subproblem (<112,16>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 13 clauses. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.01) seconds. % Length of proof is 20. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 23. 1 Point(W). [clausify]. 3 Object(c1). [clausify]. 5 - Object(x) | - Point(y) | - Ex1(B,x,y) | - Ex1(A,x,y). [clausify]. 7 - Property(x) | Enc(c1,x) | - Implies(B,x). [clausify]. 9 - Property(x) | - Object(y) | - Enc(y,x) | Ex1(x,y,W). [clausify]. 14 - Object(x) | - Ex1(B,x,W) | - Ex1(A,x,W). [resolve(5,b,1,a)]. 20 - Property(x) | - Enc(c1,x) | Ex1(x,c1,W). [resolve(9,b,3,a)]. 21 - Ex1(B,c1,W) | - Ex1(A,c1,W). [resolve(14,a,3,a)]. 25 - Property(x) | Ex1(x,c1,W) | - Property(x) | - Implies(B,x). [resolve(20,b,7,b)]. 26 Property(B). [clausify]. 27 Ex1(A,c1,W). [clausify]. 28 - Property(x) | - Property(y) | Implies(x,y) | Ex1(x,f1(x,y),f2(x,y)). [clausify]. 29 - Property(x) | - Property(y) | Implies(x,y) | - Ex1(y,f1(x,y),f2(x,y)). [clausify]. 32 - Ex1(B,c1,W). [copy(21),unit_del(b,27)]. 35 - Property(x) | Ex1(x,c1,W) | - Implies(B,x). [copy(25),merge(c)]. 36 - Property(x) | Implies(x,x) | Ex1(x,f1(x,x),f2(x,x)). [factor(28,a,b)]. 37 - Property(x) | Implies(x,x) | - Ex1(x,f1(x,x),f2(x,x)). [factor(29,a,b)]. 53 - Implies(B,B). [ur(35,a,26,a,b,32,a)]. 54 Ex1(B,f1(B,B),f2(B,B)). [resolve(36,a,26,a),unit_del(a,53)]. 56 $F. [ur(37,a,26,a,b,53,a),unit_del(a,54)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=23. Generated=50. Kept=30. proofs=1. Usable=23. Sos=7. Demods=0. Denials=0. Limbo=0, Disabled=25. Hints=0. Megabytes=0.06. User_CPU=0.00, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3671 exit (max_proofs) Wed Jun 14 16:56:49 2006