============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3755 was started by zalta on mally, Wed Jun 14 17:09:59 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 (9 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 25 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 34. % Level of proof is 10. % Maximum clause weight is 15. % Given clauses 38. 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]. 22 - Object(x) | - Proposition(y) | - Point(z) | - Ex1At(VAC(y),x,z) | True(y,z). [clausify]. 23 - Object(x) | - Proposition(y) | - Point(z) | Ex1At(VAC(y),x,z) | - True(y,z). [clausify]. 67 World(ALPHA). [clausify]. 68 Proposition(c1). [clausify]. 69 TrueIn(c1,ALPHA) | Ex1At(VAC(c1),ALPHA,W). [clausify]. 70 - TrueIn(c1,ALPHA) | - Ex1At(VAC(c1),ALPHA,W). [clausify]. 71 - World(x) | Object(x). [clausify]. 72 - Proposition(x) | Proposition(~ x). [clausify]. 74 - Object(x) | - World(x) | - Proposition(y) | TrueIn(y,x) | - True(y,f2(x)). [clausify]. 75 - Proposition(x) | - True(~ x,W) | - True(x,W). [resolve(7,a,1,a)]. 78 - Proposition(x) | True(~ x,f2(y)) | True(x,f2(y)) | - Object(y) | - World(y). [resolve(17,a,12,c)]. 79 - Object(x) | - Proposition(y) | - Ex1At(VAC(y),x,W) | True(y,W). [resolve(22,c,1,a)]. 81 - Object(x) | - Proposition(y) | Ex1At(VAC(y),x,W) | - True(y,W). [resolve(23,c,1,a)]. 83 - Object(ALPHA) | - Proposition(x) | - TrueIn(x,ALPHA) | True(x,W). [resolve(18,b,3,a)]. 92 Object(ALPHA). [resolve(71,a,67,a)]. 93 - Proposition(x) | - TrueIn(x,ALPHA) | True(x,W). [back_unit_del(83),unit_del(a,92)]. 94 Proposition(~ c1). [resolve(72,a,68,a)]. 96 True(~ c1,f2(x)) | True(c1,f2(x)) | - Object(x) | - World(x). [resolve(78,a,68,a)]. 97 True(c1,W) | TrueIn(c1,ALPHA). [resolve(79,c,69,b),unit_del(a,92),unit_del(b,68)]. 101 True(c1,W). [resolve(97,b,93,b),merge(c),unit_del(b,68)]. 103 - True(~ c1,W). [ur(75,a,68,a,c,101,a)]. 107 True(~ c1,f2(ALPHA)) | True(c1,f2(ALPHA)). [resolve(96,d,67,a),unit_del(c,92)]. 108 - TrueIn(~ c1,ALPHA). [ur(93,a,94,a,c,103,a)]. 110 - True(~ c1,f2(ALPHA)). [ur(74,a,92,a,b,67,a,c,94,a,d,108,a)]. 111 True(c1,f2(ALPHA)). [back_unit_del(107),unit_del(a,110)]. 114 TrueIn(c1,ALPHA). [resolve(111,a,74,e),unit_del(a,92),unit_del(b,67),unit_del(c,68)]. 115 - Ex1At(VAC(c1),ALPHA,W). [back_unit_del(70),unit_del(a,114)]. 118 $F. [ur(81,b,68,a,c,115,a,d,101,a),unit_del(a,92)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=38. Generated=78. Kept=51. proofs=1. Usable=35. Sos=9. Demods=0. Denials=0. Limbo=0, Disabled=70. Hints=0. Megabytes=0.10. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3755 exit (max_proofs) Wed Jun 14 17:09:59 2006