============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 30388 was started by zalta on mally, Fri Sep 11 17:11:58 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 (11 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 20 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 33. % Level of proof is 9. % Maximum clause weight is 16. % Given clauses 22. 3 Proposition(c1). [clausify]. 4 NecessarilyTrue(x) | Point(f2(x)). [clausify]. 5 - NecessarilyTrue(c1). [clausify]. 6 - WorldAt(x,y) | Object(x). [clausify]. 9 World(x) | - WorldAt(x,W). [clausify]. 10 - World(x) | TrueIn(c1,x). [clausify]. 12 - Point(x) | ActualAt(f1(x),x). [clausify]. 13 NecessarilyTrue(x) | - True(x,f2(x)). [clausify]. 15 - TrueIn(x,y) | TrueInAt(x,y,W). [clausify]. 17 - Object(x) | - Point(y) | - WorldAt(x,y) | - Point(z) | WorldAt(x,z). [clausify]. 18 - Object(x) | - Proposition(y) | - Point(z) | - TrueInAt(y,x,z) | - Point(u) | TrueInAt(y,x,u). [clausify]. 19 - Object(x) | - Point(y) | - WorldAt(x,y) | - ActualAt(x,y) | - Proposition(z) | - TrueInAt(z,x,y) | True(z,y). [clausify]. 21 - Object(x) | - Point(y) | - TrueInAt(c1,x,y) | - Point(z) | TrueInAt(c1,x,z). [resolve(18,b,3,a)]. 22 - Object(x) | - Point(y) | - WorldAt(x,y) | - ActualAt(x,y) | - TrueInAt(c1,x,y) | True(c1,y). [resolve(19,e,3,a)]. 28 - Point(x) | - WorldAt(y,x) | - Point(z) | WorldAt(y,z) | - WorldAt(y,u). [resolve(17,a,6,b)]. 30 - Point(x) | - WorldAt(y,x) | - ActualAt(y,x) | - TrueInAt(c1,y,x) | True(c1,x) | - WorldAt(y,z). [resolve(22,a,6,b)]. 32 TrueIn(c1,x) | - WorldAt(x,W). [resolve(10,a,9,a)]. 33 - Point(x) | - WorldAt(f1(x),x) | - TrueInAt(c1,f1(x),x) | True(c1,x) | - WorldAt(f1(x),y) | - Point(x). [resolve(30,c,12,b)]. 36 Point(W). [clausify]. 38 - Point(x) | WorldAt(f1(x),x). [clausify]. 39 Point(f2(c1)). [resolve(5,a,4,a)]. 40 - True(c1,f2(c1)). [resolve(13,a,5,a)]. 43 - Point(x) | - WorldAt(y,x) | - Point(z) | WorldAt(y,z) | - WorldAt(y,u). [copy(28)]. 44 - Point(x) | - TrueInAt(c1,y,x) | - Point(z) | TrueInAt(c1,y,z) | - WorldAt(y,u). [resolve(21,a,6,b)]. 45 - Point(x) | - WorldAt(f1(x),x) | - TrueInAt(c1,f1(x),x) | True(c1,x) | - WorldAt(f1(x),y). [copy(33),merge(f)]. 47 - WorldAt(x,W) | TrueInAt(c1,x,W). [resolve(32,a,15,a)]. 48 - Point(x) | - WorldAt(y,x) | - Point(z) | WorldAt(y,z). [factor(43,b,e)]. 49 - Point(x) | - WorldAt(f1(x),x) | - TrueInAt(c1,f1(x),x) | True(c1,x). [factor(45,b,e)]. 52 WorldAt(f1(f2(c1)),f2(c1)). [resolve(39,a,38,a)]. 60 - TrueInAt(c1,f1(f2(c1)),f2(c1)). [ur(49,a,39,a,b,52,a,d,40,a)]. 61 - TrueInAt(c1,f1(f2(c1)),W). [ur(44,a,36,a,c,39,a,d,60,a,e,52,a)]. 62 - WorldAt(f1(f2(c1)),W). [ur(47,b,61,a)]. 64 $F. [ur(48,b,52,a,c,36,a,d,62,a),unit_del(a,39)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=46. Kept=28. proofs=1. Usable=22. Sos=3. Demods=0. Denials=0. Limbo=0, Disabled=38. Hints=0. Megabytes=0.06. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 30388 exit (max_proofs) Fri Sep 11 17:11:58 2009