============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3750 was started by zalta on mally, Wed Jun 14 17:09:35 2006 The command was "prove". ============================== 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 (8 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 23 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.01 (+ 0.01) seconds. % Length of proof is 27. % Level of proof is 7. % Maximum clause weight is 15. % Given clauses 28. 1 Point(W). [clausify]. 3 Actual(ALPHA). [clausify]. 7 - Point(x) | - Proposition(y) | - True(~ y,x) | - True(y,x). [clausify]. 12 - Object(x) | - World(x) | Point(f2(x)). [clausify]. 17 - Point(x) | - Proposition(y) | True(~ y,x) | True(y,x). [clausify]. 18 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 61 World(ALPHA). [clausify]. 62 Proposition(c1). [clausify]. 63 True(c1,W) | TrueIn(c1,ALPHA). [clausify]. 64 - True(c1,W) | - TrueIn(c1,ALPHA). [clausify]. 65 - World(x) | Object(x). [clausify]. 66 - Proposition(x) | Proposition(~ x). [clausify]. 68 - Object(x) | - World(x) | - Proposition(y) | TrueIn(y,x) | - True(y,f2(x)). [clausify]. 69 - Proposition(x) | - True(~ x,W) | - True(x,W). [resolve(7,a,1,a)]. 72 - Proposition(x) | True(~ x,f2(y)) | True(x,f2(y)) | - Object(y) | - World(y). [resolve(17,a,12,c)]. 73 - Object(ALPHA) | - Proposition(x) | - TrueIn(x,ALPHA) | True(x,W). [resolve(18,b,3,a)]. 80 Object(ALPHA). [resolve(65,a,61,a)]. 81 - Proposition(x) | - TrueIn(x,ALPHA) | True(x,W). [back_unit_del(73),unit_del(a,80)]. 82 Proposition(~ c1). [resolve(66,a,62,a)]. 85 True(~ c1,f2(x)) | True(c1,f2(x)) | - Object(x) | - World(x). [resolve(72,a,62,a)]. 92 True(c1,W). [resolve(81,b,63,b),merge(c),unit_del(a,62)]. 93 - TrueIn(c1,ALPHA). [back_unit_del(64),unit_del(a,92)]. 94 - True(c1,f2(ALPHA)). [ur(68,a,80,a,b,61,a,c,62,a,d,93,a)]. 95 - True(~ c1,W). [ur(69,a,62,a,c,92,a)]. 99 True(~ c1,f2(ALPHA)). [resolve(85,d,61,a),unit_del(b,94),unit_del(c,80)]. 100 - TrueIn(~ c1,ALPHA). [ur(81,a,82,a,c,95,a)]. 101 $F. [ur(68,a,80,a,b,61,a,c,82,a,d,100,a),unit_del(a,99)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=28. Generated=56. Kept=40. proofs=1. Usable=26. Sos=5. Demods=0. Denials=0. Limbo=0, Disabled=66. Hints=0. Megabytes=0.08. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3750 exit (max_proofs) Wed Jun 14 17:09:35 2006