============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 13566 was started by zalta on mally, Sat Jul 21 16:05:50 2007 The command was "prove.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(sos). % not echoed (5 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 13. % Level of proof is 5. % Maximum clause weight is 4. % Given clauses 4. 1 Proposition(L). [clausify]. 2 - True(L,W). [clausify]. 5 - Proposition(x) | Actual(f2(x)). [clausify]. 7 - Proposition(x) | TrueIn(x,f2(x)). [clausify]. 11 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 14 TrueIn(L,f2(L)). [resolve(7,a,1,a)]. 18 - Object(x) | - Actual(x) | - TrueIn(L,x) | True(L,W). [resolve(11,c,1,a)]. 20 - Object(x) | - Actual(x) | - TrueIn(L,x). [resolve(18,d,2,a)]. 22 - Object(f2(L)) | - Actual(f2(L)). [resolve(20,c,14,a)]. 24 - Actual(x) | Object(x). [clausify]. 27 Actual(f2(L)). [resolve(5,a,1,a)]. 30 - Object(f2(L)). [copy(22),unit_del(b,27)]. 32 $F. [resolve(27,a,24,a),unit_del(a,30)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=4. Generated=9. Kept=8. proofs=1. Usable=4. Sos=4. Demods=0. Denials=0. Limbo=0, Disabled=23. 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 13566 exit (max_proofs) Sat Jul 21 16:05:50 2007