============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3744 was started by zalta on mally, Wed Jun 14 17:09:02 2006 The command was "prove". ============================== 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 (4 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 16 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.01) seconds. % Length of proof is 28. % Level of proof is 5. % Maximum clause weight is 7. % Given clauses 9. 1 World(c1). [clausify]. 2 - Possible(c1). [clausify]. 3 - World(x) | Object(x). [clausify]. 4 - Object(x) | - World(x) | Situation(x). [clausify]. 6 - Object(x) | - World(x) | Point(f1(x)). [clausify]. 9 - Object(x) | Possible(x) | - Situation(x) | - Point(y) | Proposition(f4(x,y)). [clausify]. 10 - Object(x) | - World(x) | - Proposition(y) | - TrueIn(y,x) | True(y,f1(x)). [clausify]. 13 - Object(x) | Possible(x) | - Situation(x) | - Point(y) | TrueIn(f4(x,y),x). [clausify]. 14 - Object(x) | Possible(x) | - Situation(x) | - Point(y) | - True(f4(x,y),y). [clausify]. 18 - Object(c1) | Situation(c1). [resolve(4,b,1,a)]. 19 - Object(c1) | Point(f1(c1)). [resolve(6,b,1,a)]. 21 - Object(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,f1(c1)). [resolve(10,b,1,a)]. 31 - Object(c1) | - Situation(c1) | - Point(x) | Proposition(f4(c1,x)). [resolve(9,b,2,a)]. 34 - Object(c1) | - Situation(c1) | - Point(x) | TrueIn(f4(c1,x),c1). [resolve(13,b,2,a)]. 37 - Object(c1) | - Situation(c1) | - Point(x) | - True(f4(c1,x),x). [resolve(14,b,2,a)]. 49 - Object(c1) | - Point(x) | Proposition(f4(c1,x)) | - Object(c1). [resolve(31,b,18,b)]. 52 - Object(c1) | - Point(x) | TrueIn(f4(c1,x),c1) | - Object(c1). [resolve(34,b,18,b)]. 55 - Object(c1) | - Point(x) | - True(f4(c1,x),x) | - Object(c1). [resolve(37,b,18,b)]. 58 Object(c1). [resolve(3,a,1,a)]. 59 Point(f1(c1)). [copy(19),unit_del(a,58)]. 60 - Proposition(x) | - TrueIn(x,c1) | True(x,f1(c1)). [copy(21),unit_del(a,58)]. 62 - Point(x) | Proposition(f4(c1,x)). [copy(49),merge(d),unit_del(a,58)]. 63 - Point(x) | TrueIn(f4(c1,x),c1). [copy(52),merge(d),unit_del(a,58)]. 64 - Point(x) | - True(f4(c1,x),x). [copy(55),merge(d),unit_del(a,58)]. 65 Proposition(f4(c1,f1(c1))). [resolve(62,a,59,a)]. 66 TrueIn(f4(c1,f1(c1)),c1). [resolve(63,a,59,a)]. 67 - True(f4(c1,f1(c1)),f1(c1)). [ur(64,a,59,a)]. 68 $F. [ur(60,a,65,a,c,67,a),unit_del(a,66)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=9. Generated=20. Kept=10. proofs=1. Usable=9. Sos=1. Demods=0. Denials=0. Limbo=0, Disabled=51. Hints=0. Megabytes=0.05. User_CPU=0.00, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3744 exit (max_proofs) Wed Jun 14 17:09:02 2006