============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 30335 was started by zalta on mally, Fri Sep 11 16:58:40 2009 The command was "prover9.orig". ============================== 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). clear(fof_reduction). % formulas(usable). % not echoed (2 formulas) % formulas(sos). % not echoed (1 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 11 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.00) seconds. % Length of proof is 19. % Level of proof is 6. % Maximum clause weight is 3. % Given clauses 8. 1 - Object(x) | - Property(y) | - Point(z) | - EncAt(x,y,z) | - Point(u) | EncAt(x,y,u). [clausify]. 2 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | Property(f1(x,y,z)). [clausify]. 3 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | VAC(y) = f1(x,y,z). [clausify]. 4 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | EncAt(x,f1(x,y,z),z). [clausify]. 5 - Object(x) | - Proposition(y) | - Point(z) | EncpAt(x,y,z) | - Property(u) | VAC(y) != u | - EncAt(x,u,z). [clausify]. 12 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | f1(x,y,z) = VAC(y). [copy(3),flip(e)]. 13 Object(c1). [clausify]. 14 Proposition(c2). [clausify]. 15 Point(c3). [clausify]. 16 Point(c4). [clausify]. 17 EncpAt(c1,c2,c3). [clausify]. 18 - EncpAt(c1,c2,c4). [clausify]. 19 EncAt(c1,f1(c1,c2,c3),c3). [hyper(4,a,13,a,b,14,a,c,15,a,d,17,a)]. 20 f1(c1,c2,c3) = VAC(c2). [hyper(12,a,13,a,b,14,a,c,15,a,d,17,a)]. 21 Property(VAC(c2)). [hyper(2,a,13,a,b,14,a,c,15,a,d,17,a),demod(20(4))]. 22 EncAt(c1,VAC(c2),c3). [back_demod(19),demod(20(5))]. 23 - EncAt(c1,VAC(c2),c4). [ur(5,a,13,a,b,14,a,c,16,a,d,18,a,e,21,a,f,xx)]. 24 - EncAt(c1,VAC(c2),c3). [ur(1,a,13,a,b,21,a,c,15,a,e,16,a,f,23,a)]. 25 $F. [resolve(24,a,22,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=8. Generated=13. Kept=12. proofs=1. Usable=13. Sos=2. Demods=1. Denials=0. Limbo=0, Disabled=8. Hints=0. Megabytes=0.04. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 30335 exit (max_proofs) Fri Sep 11 16:58:40 2009