============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 13565 was started by zalta on mally, Sat Jul 21 16:05:46 2007 The command was "prove.orig". ============================== end of head =========================== ============================== INPUT ================================= op(300,prefix,~). 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(sos). % not echoed (6 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 15 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 20. % Level of proof is 5. % Maximum clause weight is 9. % Given clauses 5. 1 Point(W). [clausify]. 3 Actual(c1). [clausify]. 5 TrueIn(c2,c1). [clausify]. 6 TrueIn(~ c2,c1). [clausify]. 7 - Point(x) | - Proposition(y) | - True(~ y,x) | - True(y,x). [clausify]. 8 - Actual(x) | Object(x). [clausify]. 15 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 21 Object(c1). [resolve(8,a,3,a)]. 22 - Object(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,W). [resolve(15,b,3,a)]. 26 - Object(c1) | - Proposition(c2) | True(c2,W). [resolve(22,c,5,a)]. 27 - Object(c1) | - Proposition(~ c2) | True(~ c2,W). [resolve(22,c,6,a)]. 28 - Proposition(c2) | True(c2,W). [resolve(26,a,21,a)]. 30 Proposition(c2). [clausify]. 31 - Proposition(x) | Proposition(~ x). [clausify]. 32 - Proposition(x) | - True(~ x,W) | - True(x,W). [resolve(7,a,1,a)]. 34 True(c2,W). [copy(28),unit_del(a,30)]. 35 - Proposition(~ c2) | True(~ c2,W). [resolve(27,a,21,a)]. 36 Proposition(~ c2). [resolve(31,a,30,a)]. 37 True(~ c2,W). [back_unit_del(35),unit_del(a,36)]. 38 $F. [ur(32,a,30,a,c,34,a),unit_del(a,37)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=5. Generated=10. Kept=8. proofs=1. Usable=5. Sos=2. Demods=0. Denials=0. Limbo=0, Disabled=27. Hints=0. Megabytes=0.03. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13565 exit (max_proofs) Sat Jul 21 16:05:46 2007