============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3740 was started by zalta on mally, Wed Jun 14 17:08:37 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 (7 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 23 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 60. % Level of proof is 22. % Maximum clause weight is 12. % Given clauses 60. 1 Object(c1). [clausify]. 4 - Proposition(x) | Property(VAC(x)). [clausify]. 7 - Property(x) | - Enc(c1,x) | Proposition(f5(x)). [clausify]. 9 - Object(x) | Maximal2(x) | - Situation(x) | Proposition(f4(x)). [clausify]. 11 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 12 - Object(x) | Maximal2(x) | - Situation(x) | - TrueIn(f4(x),x). [clausify]. 15 - Object(x) | Situation(x) | - Ex1(A,x,W) | Property(f3(x)). [clausify]. 16 - Property(x) | Enc(c1,x) | - Proposition(y) | VAC(y) != x. [clausify]. 18 - Object(x) | Situation(x) | - Ex1(A,x,W) | Enc(x,f3(x)). [clausify]. 22 - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(y) | VAC(y) != f3(x). [clausify]. 23 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 27 Maximal2(c1) | - Situation(c1) | Proposition(f4(c1)). [resolve(9,a,1,a)]. 29 - Proposition(x) | TrueIn(x,c1) | - Encp(c1,x). [resolve(11,a,1,a)]. 32 Situation(c1) | - Ex1(A,c1,W) | Property(f3(c1)). [resolve(15,a,1,a)]. 34 Situation(c1) | - Ex1(A,c1,W) | Enc(c1,f3(c1)). [resolve(18,a,1,a)]. 38 Situation(c1) | - Ex1(A,c1,W) | - Proposition(x) | VAC(x) != f3(c1). [resolve(22,a,1,a)]. 39 - Proposition(x) | Encp(c1,x) | - Property(y) | VAC(x) != y | - Enc(c1,y). [resolve(23,a,1,a)]. 63 Situation(c1) | - Ex1(A,c1,W) | VAC(f5(x)) != f3(c1) | - Property(x) | - Enc(c1,x). [resolve(38,c,7,c)]. 67 Ex1(A,c1,W). [clausify]. 68 - Situation(x) | - Maximal2(x). [clausify]. 69 - Property(x) | - Enc(c1,x) | VAC(f5(x)) = x. [clausify]. 71 Maximal2(c1) | - Situation(c1) | - TrueIn(f4(c1),c1). [resolve(12,a,1,a)]. 72 Situation(c1) | Property(f3(c1)). [copy(32),unit_del(b,67)]. 73 Situation(c1) | Enc(c1,f3(c1)). [copy(34),unit_del(b,67)]. 78 Maximal2(c1) | - Situation(c1) | Property(VAC(f4(c1))). [resolve(27,c,4,a)]. 79 Maximal2(c1) | - Situation(c1) | - Property(x) | Enc(c1,x) | VAC(f4(c1)) != x. [resolve(27,c,16,c)]. 82 TrueIn(f4(c1),c1) | - Encp(c1,f4(c1)) | Maximal2(c1) | - Situation(c1). [resolve(29,a,27,c)]. 96 Situation(c1) | VAC(f5(x)) != f3(c1) | - Property(x) | - Enc(c1,x). [copy(63),unit_del(b,67)]. 98 Encp(c1,f4(c1)) | - Property(x) | VAC(f4(c1)) != x | - Enc(c1,x) | Maximal2(c1) | - Situation(c1). [resolve(39,a,27,c)]. 102 Situation(c1) | - Property(f3(c1)) | VAC(f5(f3(c1))) = f3(c1). [resolve(73,b,69,b)]. 105 Maximal2(c1) | Property(VAC(f4(c1))) | Property(f3(c1)). [resolve(78,b,72,a)]. 106 Maximal2(c1) | - Situation(c1) | - Property(VAC(f4(c1))) | Enc(c1,VAC(f4(c1))). [xx_res(79,e)]. 109 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | - Enc(c1,VAC(f4(c1))) | Maximal2(c1) | - Situation(c1). [xx_res(98,c)]. 111 Property(VAC(f4(c1))) | Property(f3(c1)) | - Situation(c1). [resolve(105,a,68,b)]. 112 Property(VAC(f4(c1))) | Property(f3(c1)). [resolve(111,c,72,a),merge(c)]. 113 Maximal2(c1) | - Property(VAC(f4(c1))) | Enc(c1,VAC(f4(c1))) | Property(f3(c1)). [resolve(106,b,72,a)]. 114 Maximal2(c1) | Enc(c1,VAC(f4(c1))) | Property(f3(c1)). [resolve(113,b,112,a),merge(d)]. 119 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | Maximal2(c1) | - Situation(c1) | Property(f3(c1)). [resolve(109,c,114,b),merge(e)]. 120 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | Maximal2(c1) | Property(f3(c1)). [resolve(119,d,72,a),merge(e)]. 123 Encp(c1,f4(c1)) | Maximal2(c1) | Property(f3(c1)). [resolve(120,b,112,a),merge(d)]. 127 Maximal2(c1) | Property(f3(c1)) | TrueIn(f4(c1),c1) | - Situation(c1). [resolve(123,a,82,b),merge(d)]. 128 Maximal2(c1) | Property(f3(c1)) | TrueIn(f4(c1),c1). [resolve(127,d,72,a),merge(d)]. 129 Maximal2(c1) | Property(f3(c1)) | - Situation(c1). [resolve(128,c,71,c),merge(c)]. 130 Maximal2(c1) | Property(f3(c1)). [resolve(129,c,72,a),merge(c)]. 131 Property(f3(c1)) | - Situation(c1). [resolve(130,a,68,b)]. 132 Property(f3(c1)). [resolve(131,b,72,a),merge(b)]. 135 Situation(c1) | VAC(f5(f3(c1))) = f3(c1). [back_unit_del(102),unit_del(b,132)]. 139 Situation(c1) | - Enc(c1,f3(c1)). [resolve(135,b,96,b),merge(b),unit_del(b,132)]. 140 Situation(c1). [resolve(139,b,73,b),merge(b)]. 142 Encp(c1,f4(c1)) | - Property(VAC(f4(c1))) | - Enc(c1,VAC(f4(c1))) | Maximal2(c1). [back_unit_del(109),unit_del(e,140)]. 144 Maximal2(c1) | - Property(VAC(f4(c1))) | Enc(c1,VAC(f4(c1))). [back_unit_del(106),unit_del(b,140)]. 158 TrueIn(f4(c1),c1) | - Encp(c1,f4(c1)) | Maximal2(c1). [back_unit_del(82),unit_del(d,140)]. 160 Maximal2(c1) | Property(VAC(f4(c1))). [back_unit_del(78),unit_del(b,140)]. 162 Maximal2(c1) | - TrueIn(f4(c1),c1). [back_unit_del(71),unit_del(b,140)]. 163 - Maximal2(c1). [ur(68,a,140,a)]. 164 - TrueIn(f4(c1),c1). [back_unit_del(162),unit_del(a,163)]. 165 Property(VAC(f4(c1))). [back_unit_del(160),unit_del(a,163)]. 167 - Encp(c1,f4(c1)). [back_unit_del(158),unit_del(a,164),unit_del(c,163)]. 169 Enc(c1,VAC(f4(c1))). [back_unit_del(144),unit_del(a,163),unit_del(b,165)]. 170 $F. [back_unit_del(142),unit_del(a,167),unit_del(b,165),unit_del(c,169),unit_del(d,163)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=60. Generated=134. Kept=103. proofs=1. Usable=16. Sos=12. Demods=0. Denials=0. Limbo=7, Disabled=133. Hints=0. Megabytes=0.14. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3740 exit (max_proofs) Wed Jun 14 17:08:37 2006