============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3741 was started by zalta on mally, Wed Jun 14 17:08:41 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 (8 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 24 clauses. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.01) seconds. % Length of proof is 28. % Level of proof is 8. % Maximum clause weight is 12. % Given clauses 43. 1 Proposition(L). [clausify]. 4 - Situation(x) | - Partial2(x). [clausify]. 6 - Property(x) | - Enc(c1,x) | x != x. [clausify]. 8 - Object(x) | Partial2(x) | Maximal2(x). [clausify]. 11 - Object(x) | - Maximal2(x) | - Proposition(y) | TrueIn(y,x). [clausify]. 13 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 16 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f1(x,y)). [clausify]. 18 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 50 Object(c1). [clausify]. 51 Ex1At(A,c1,W). [clausify]. 52 - Property(x) | - Enc(c1,x). [copy(6),xx(c)]. 56 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Property(f3(x)). [clausify]. 57 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Enc(x,f3(x)). [clausify]. 59 - Object(x) | - Maximal2(x) | TrueIn(L,x). [resolve(11,c,1,a)]. 61 - Object(x) | - TrueIn(L,x) | Encp(x,L). [resolve(13,b,1,a)]. 65 - Object(x) | - Encp(x,L) | Property(f1(x,L)). [resolve(16,b,1,a)]. 67 - Object(x) | - Encp(x,L) | Enc(x,f1(x,L)). [resolve(18,b,1,a)]. 83 - Object(x) | Maximal2(x) | - Situation(x). [resolve(8,b,4,b)]. 93 Situation(c1) | Property(f3(c1)). [resolve(56,c,51,a),unit_del(a,50)]. 94 Situation(c1) | Enc(c1,f3(c1)). [resolve(57,c,51,a),unit_del(a,50)]. 98 Situation(c1) | - Property(f3(c1)). [resolve(94,b,52,b)]. 99 Situation(c1). [resolve(98,b,93,b),merge(b)]. 100 Maximal2(c1). [resolve(99,a,83,c),unit_del(a,50)]. 101 TrueIn(L,c1). [resolve(100,a,59,b),unit_del(a,50)]. 102 Encp(c1,L). [resolve(101,a,61,b),unit_del(a,50)]. 104 Enc(c1,f1(c1,L)). [resolve(102,a,67,b),unit_del(a,50)]. 105 Property(f1(c1,L)). [resolve(102,a,65,b),unit_del(a,50)]. 121 $F. [resolve(104,a,52,b),unit_del(a,105)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=43. Generated=101. Kept=71. proofs=1. Usable=36. Sos=8. Demods=2. Denials=0. Limbo=11, Disabled=65. Hints=0. Megabytes=0.12. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3741 exit (max_proofs) Wed Jun 14 17:08:41 2006