============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 30387 was started by zalta on mally, Fri Sep 11 17:11:52 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(sos). % not echoed (8 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 22 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 28. % Level of proof is 6. % Maximum clause weight is 8. % Given clauses 7. 2 Proposition(c1). [clausify]. 3 NecessarilyTrue(c1). [clausify]. 4 World(c2). [clausify]. 6 - TrueIn(c1,c2). [clausify]. 7 - WorldAt(x,y) | Object(x). [clausify]. 9 - World(x) | WorldAt(x,W). [clausify]. 12 - NecessarilyTrue(x) | - Point(y) | True(x,y). [clausify]. 14 TrueIn(x,y) | - TrueInAt(x,y,W). [clausify]. 16 - Object(x) | - Point(y) | - WorldAt(x,y) | Point(f1(x,y)). [clausify]. 17 - Object(x) | - Proposition(y) | - Point(z) | - TrueInAt(y,x,z) | - Point(u) | TrueInAt(y,x,u). [clausify]. 20 - Object(x) | - Point(y) | - WorldAt(x,y) | - Proposition(z) | TrueInAt(z,x,f1(x,y)) | - True(z,f1(x,y)). [clausify]. 23 - Object(x) | - Point(y) | - TrueInAt(c1,x,y) | - Point(z) | TrueInAt(c1,x,z). [resolve(17,b,2,a)]. 27 - Object(x) | - Point(y) | - WorldAt(x,y) | TrueInAt(c1,x,f1(x,y)) | - True(c1,f1(x,y)). [resolve(20,d,2,a)]. 32 WorldAt(c2,W). [resolve(9,a,4,a)]. 34 Object(c2). [resolve(32,a,7,a)]. 36 - Object(c2) | - Point(W) | Point(f1(c2,W)). [resolve(32,a,16,c)]. 38 - Object(c2) | - Point(W) | TrueInAt(c1,c2,f1(c2,W)) | - True(c1,f1(c2,W)). [resolve(32,a,27,c)]. 40 - Point(W) | Point(f1(c2,W)). [resolve(36,a,34,a)]. 42 - Point(W) | TrueInAt(c1,c2,f1(c2,W)) | - True(c1,f1(c2,W)). [resolve(38,a,34,a)]. 43 Point(W). [clausify]. 44 - Point(x) | True(c1,x). [resolve(12,a,3,a)]. 47 - TrueInAt(c1,c2,W). [resolve(14,a,6,a)]. 48 - Point(x) | - TrueInAt(c1,c2,x) | - Point(y) | TrueInAt(c1,c2,y). [resolve(34,a,23,a)]. 49 Point(f1(c2,W)). [copy(40),unit_del(a,43)]. 51 TrueInAt(c1,c2,f1(c2,W)) | - True(c1,f1(c2,W)). [copy(42),unit_del(a,43)]. 55 True(c1,f1(c2,W)). [resolve(49,a,44,a)]. 56 - TrueInAt(c1,c2,f1(c2,W)). [ur(48,a,49,a,c,43,a,d,47,a)]. 57 $F. [back_unit_del(51),unit_del(a,56),unit_del(b,55)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=7. Generated=18. Kept=14. proofs=1. Usable=7. Sos=3. Demods=0. Denials=0. Limbo=2, Disabled=44. Hints=0. Megabytes=0.05. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 30387 exit (max_proofs) Fri Sep 11 17:11:52 2009