============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3739 was started by zalta on mally, Wed Jun 14 17:08:29 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 (9 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 26 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 38. % Level of proof is 14. % Maximum clause weight is 8. % Given clauses 30. 2 Object(c1). [clausify]. 6 - Property(x) | - Enc(c1,x) | x != x. [clausify]. 9 - Object(x) | Partial1(x) | Maximal1(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]. 17 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Property(f3(x)). [clausify]. 19 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 20 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Enc(x,f3(x)). [clausify]. 23 - Object(x) | - Maximal1(x) | - Proposition(y) | TrueIn(y,x) | TrueIn(~ y,x). [clausify]. 35 - Proposition(x) | - Encp(c1,x) | Property(f1(c1,x)). [resolve(16,a,2,a)]. 36 Situation(c1) | - Ex1At(A,c1,W) | Property(f3(c1)). [resolve(17,a,2,a)]. 39 Situation(c1) | - Ex1At(A,c1,W) | Enc(c1,f3(c1)). [resolve(20,a,2,a)]. 46 - Proposition(x) | - Encp(c1,x) | - Enc(c1,f1(c1,x)) | f1(c1,x) != f1(c1,x). [resolve(35,c,6,a)]. 48 Situation(c1) | - Ex1At(A,c1,W) | - Enc(c1,f3(c1)) | f3(c1) != f3(c1). [resolve(36,c,6,a)]. 54 Proposition(L). [clausify]. 55 Ex1At(A,c1,W). [clausify]. 56 - Situation(x) | - Partial1(x). [clausify]. 57 - Proposition(x) | Proposition(~ x). [clausify]. 60 Partial1(c1) | Maximal1(c1). [resolve(9,a,2,a)]. 62 - Proposition(x) | - TrueIn(x,c1) | Encp(c1,x). [resolve(13,a,2,a)]. 66 - Proposition(x) | - Encp(c1,x) | Enc(c1,f1(c1,x)). [resolve(19,a,2,a)]. 67 Situation(c1) | Enc(c1,f3(c1)). [copy(39),unit_del(b,55)]. 69 - Maximal1(c1) | - Proposition(x) | TrueIn(x,c1) | TrueIn(~ x,c1). [resolve(23,a,2,a)]. 71 - Proposition(x) | - Encp(c1,x) | - Enc(c1,f1(c1,x)). [copy(46),xx(d)]. 72 Situation(c1) | - Enc(c1,f3(c1)). [copy(48),xx(d),unit_del(b,55)]. 73 Proposition(~ L). [resolve(57,a,54,a)]. 74 Maximal1(c1) | - Situation(c1). [resolve(60,a,56,b)]. 75 Situation(c1). [resolve(72,b,67,b),merge(b)]. 76 Maximal1(c1). [back_unit_del(74),unit_del(b,75)]. 77 - Proposition(x) | TrueIn(x,c1) | TrueIn(~ x,c1). [back_unit_del(69),unit_del(a,76)]. 81 TrueIn(L,c1) | TrueIn(~ L,c1). [resolve(77,a,54,a)]. 84 TrueIn(L,c1) | Encp(c1,~ L). [resolve(81,b,62,b),unit_del(b,73)]. 85 Encp(c1,~ L) | Encp(c1,L). [resolve(84,a,62,b),unit_del(b,54)]. 87 Encp(c1,L) | Enc(c1,f1(c1,~ L)). [resolve(85,a,66,b),unit_del(b,73)]. 90 Encp(c1,L) | - Encp(c1,~ L). [resolve(87,b,71,c),unit_del(b,73)]. 91 Encp(c1,L). [resolve(90,b,85,a),merge(b)]. 93 Enc(c1,f1(c1,L)). [resolve(91,a,66,b),unit_del(a,54)]. 95 $F. [ur(71,a,54,a,b,91,a),unit_del(a,93)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=30. Generated=50. Kept=41. proofs=1. Usable=19. Sos=3. Demods=1. Denials=0. Limbo=3, Disabled=67. Hints=0. Megabytes=0.07. User_CPU=0.00, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3739 exit (max_proofs) Wed Jun 14 17:08:29 2006