============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3774 was started by zalta on mally, Wed Jun 14 17:12:09 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 (6 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 21 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.01 (+ 0.01) seconds. % Length of proof is 44. % Level of proof is 8. % Maximum clause weight is 12. % Given clauses 26. 1 Proposition(c1). [clausify]. 4 - Proposition(x) | Persistent(x) | Situation(f3(x)). [clausify]. 5 - Proposition(x) | Persistent(x) | Situation(f4(x)). [clausify]. 6 - Proposition(x) | Persistent(x) | TrueIn(x,f3(x)). [clausify]. 7 - Proposition(x) | Persistent(x) | - TrueIn(x,f4(x)). [clausify]. 8 - Proposition(x) | Persistent(x) | PartOf(f3(x),f4(x)). [clausify]. 9 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 10 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 11 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f1(x,y)). [clausify]. 14 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 15 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f1(x,y). [clausify]. 16 - Object(x) | - Object(y) | - PartOf(x,y) | - Property(z) | - Enc(x,z) | Enc(y,z). [clausify]. 17 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 22 Persistent(c1) | Situation(f3(c1)). [resolve(4,a,1,a)]. 23 Persistent(c1) | Situation(f4(c1)). [resolve(5,a,1,a)]. 24 Persistent(c1) | TrueIn(c1,f3(c1)). [resolve(6,a,1,a)]. 25 Persistent(c1) | - TrueIn(c1,f4(c1)). [resolve(7,a,1,a)]. 26 Persistent(c1) | PartOf(f3(c1),f4(c1)). [resolve(8,a,1,a)]. 31 - Object(x) | - Encp(x,c1) | VAC(c1) = f1(x,c1). [resolve(15,b,1,a)]. 39 Persistent(c1) | - Object(f3(c1)) | - Object(f4(c1)) | - Property(x) | - Enc(f3(c1),x) | Enc(f4(c1),x). [resolve(26,b,16,c)]. 43 - Persistent(c1). [clausify]. 44 - Situation(x) | Object(x). [clausify]. 45 Situation(f3(c1)). [copy(22),unit_del(a,43)]. 46 Situation(f4(c1)). [copy(23),unit_del(a,43)]. 47 TrueIn(c1,f3(c1)). [copy(24),unit_del(a,43)]. 48 - TrueIn(c1,f4(c1)). [copy(25),unit_del(a,43)]. 49 - Object(x) | - TrueIn(c1,x) | Encp(x,c1). [resolve(9,b,1,a)]. 50 - Object(x) | TrueIn(c1,x) | - Encp(x,c1). [resolve(10,b,1,a)]. 51 - Object(x) | - Encp(x,c1) | Property(f1(x,c1)). [resolve(11,b,1,a)]. 52 - Object(x) | - Encp(x,c1) | Enc(x,f1(x,c1)). [resolve(14,b,1,a)]. 53 - Object(x) | - Encp(x,c1) | f1(x,c1) = VAC(c1). [copy(31),flip(c)]. 54 - Object(x) | Encp(x,c1) | - Property(y) | VAC(c1) != y | - Enc(x,y). [resolve(17,b,1,a)]. 60 - Object(f3(c1)) | - Object(f4(c1)) | - Property(x) | - Enc(f3(c1),x) | Enc(f4(c1),x). [copy(39),unit_del(a,43)]. 61 Object(f3(c1)). [resolve(45,a,44,a)]. 62 - Object(f4(c1)) | - Property(x) | - Enc(f3(c1),x) | Enc(f4(c1),x). [back_unit_del(60),unit_del(a,61)]. 65 Object(f4(c1)). [resolve(46,a,44,a)]. 68 - Property(x) | - Enc(f3(c1),x) | Enc(f4(c1),x). [back_unit_del(62),unit_del(a,65)]. 69 Encp(f3(c1),c1). [resolve(49,b,47,a),unit_del(a,61)]. 71 - Encp(f4(c1),c1). [ur(50,a,65,a,b,48,a)]. 72 f1(f3(c1),c1) = VAC(c1). [resolve(69,a,53,b),unit_del(a,61)]. 73 Enc(f3(c1),VAC(c1)). [resolve(69,a,52,b),demod(72(9)),unit_del(a,61)]. 74 Property(VAC(c1)). [resolve(69,a,51,b),demod(72(7)),unit_del(a,61)]. 76 - Enc(f4(c1),VAC(c1)). [ur(54,a,65,a,b,71,a,c,74,a,d,xx)]. 90 $F. [resolve(68,b,73,a),unit_del(a,74),unit_del(b,76)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=26. Generated=71. Kept=47. proofs=1. Usable=26. Sos=14. Demods=1. Denials=0. Limbo=0, Disabled=49. Hints=0. Megabytes=0.09. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3774 exit (max_proofs) Wed Jun 14 17:12:09 2006