============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3742 was started by zalta on mally, Wed Jun 14 17:08:48 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 (6 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 18 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 31. % Level of proof is 6. % Maximum clause weight is 11. % Given clauses 13. 1 World(c1). [clausify]. 2 - Maximal1(c1). [clausify]. 4 - World(x) | Object(x). [clausify]. 7 - Object(x) | - World(x) | Situation(x). [clausify]. 8 - Object(x) | - World(x) | Point(f2(x)). [clausify]. 9 - Object(x) | Maximal1(x) | - Situation(x) | Proposition(f1(x)). [clausify]. 10 - Object(x) | Maximal1(x) | - Situation(x) | - TrueIn(f1(x),x). [clausify]. 12 - Object(x) | Maximal1(x) | - Situation(x) | - TrueIn(~ f1(x),x). [clausify]. 16 - Object(x) | - World(x) | - Proposition(y) | TrueIn(y,x) | - True(y,f2(x)). [clausify]. 20 - Object(c1) | Situation(c1). [resolve(7,b,1,a)]. 21 - Object(c1) | Point(f2(c1)). [resolve(8,b,1,a)]. 25 - Object(c1) | - Proposition(x) | TrueIn(x,c1) | - True(x,f2(c1)). [resolve(16,b,1,a)]. 33 - Object(c1) | - Situation(c1) | Proposition(f1(c1)). [resolve(9,b,2,a)]. 34 - Object(c1) | - Situation(c1) | - TrueIn(f1(c1),c1). [resolve(10,b,2,a)]. 35 - Object(c1) | - Situation(c1) | - TrueIn(~ f1(c1),c1). [resolve(12,b,2,a)]. 48 - Object(c1) | Proposition(f1(c1)) | - Object(c1). [resolve(33,b,20,b)]. 49 - Object(c1) | - TrueIn(f1(c1),c1) | - Object(c1). [resolve(34,b,20,b)]. 50 - Object(c1) | - TrueIn(~ f1(c1),c1) | - Object(c1). [resolve(35,b,20,b)]. 55 - Proposition(x) | Proposition(~ x). [clausify]. 56 - Point(x) | - Proposition(y) | True(~ y,x) | True(y,x). [clausify]. 57 Object(c1). [resolve(4,a,1,a)]. 58 Point(f2(c1)). [copy(21),unit_del(a,57)]. 60 - Proposition(x) | TrueIn(x,c1) | - True(x,f2(c1)). [copy(25),unit_del(a,57)]. 61 Proposition(f1(c1)). [copy(48),merge(c),unit_del(a,57)]. 62 - TrueIn(f1(c1),c1). [copy(49),merge(c),unit_del(a,57)]. 63 - TrueIn(~ f1(c1),c1). [copy(50),merge(c),unit_del(a,57)]. 64 - Proposition(x) | True(~ x,f2(c1)) | True(x,f2(c1)). [resolve(58,a,56,a)]. 65 Proposition(~ f1(c1)). [resolve(61,a,55,a)]. 66 - True(f1(c1),f2(c1)). [ur(60,a,61,a,b,62,a)]. 67 True(~ f1(c1),f2(c1)). [resolve(64,a,61,a),unit_del(b,66)]. 69 $F. [ur(60,a,65,a,b,63,a),unit_del(a,67)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=13. Generated=27. Kept=15. proofs=1. Usable=13. Sos=1. Demods=0. Denials=0. Limbo=1, Disabled=50. 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 3742 exit (max_proofs) Wed Jun 14 17:08:48 2006