============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3769 was started by zalta on mally, Wed Jun 14 17:11:51 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 (5 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 42. % Level of proof is 9. % Maximum clause weight is 21. % Given clauses 62. 1 Situation(c1). [clausify]. 2 Situation(c2). [clausify]. 4 - Situation(x) | Object(x). [clausify]. 5 - Object(x) | - Situation(x) | Ex1At(A,x,W). [clausify]. 6 - Situation(x) | - PartOf(x,c1) | PartOf(x,c2). [clausify]. 7 - Situation(x) | PartOf(x,c1) | - PartOf(x,c2). [clausify]. 24 - Object(c1) | Ex1At(A,c1,W). [resolve(5,b,1,a)]. 25 - Object(c2) | Ex1At(A,c2,W). [resolve(5,b,2,a)]. 46 c2 != c1. [clausify]. 49 - Object(x) | - Object(y) | - PartOf(x,y) | - Property(z) | - Enc(x,z) | Enc(y,z). [clausify]. 50 - Ex1At(A,x,W) | - Ex1At(A,y,W) | Property(f4(x,y)) | y = x. [clausify]. 52 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | Enc(x,f3(x,y)). [clausify]. 53 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1At(A,x,W) | - Ex1At(A,y,W) | - Enc(y,f3(x,y)). [clausify]. 54 - Ex1At(A,x,W) | - Ex1At(A,y,W) | Enc(x,f4(x,y)) | Enc(y,f4(x,y)) | y = x. [clausify]. 55 - Ex1At(A,x,W) | - Ex1At(A,y,W) | - Enc(x,f4(x,y)) | - Enc(y,f4(x,y)) | y = x. [clausify]. 56 Object(c1). [resolve(4,a,1,a)]. 57 Object(c2). [resolve(4,a,2,a)]. 58 Ex1At(A,c1,W). [copy(24),unit_del(a,56)]. 59 Ex1At(A,c2,W). [copy(25),unit_del(a,57)]. 60 - PartOf(c1,c1) | PartOf(c1,c2). [resolve(6,a,1,a)]. 63 PartOf(c2,c1) | - PartOf(c2,c2). [resolve(7,a,2,a)]. 82 - Object(x) | PartOf(x,x) | - Ex1At(A,x,W) | Enc(x,f3(x,x)). [factor(52,a,b),merge(d)]. 83 - Object(x) | PartOf(x,x) | - Ex1At(A,x,W) | - Enc(x,f3(x,x)). [factor(53,a,b),merge(d)]. 84 - Ex1At(A,x,W) | - Enc(x,f4(x,c1)) | - Enc(c1,f4(x,c1)) | c1 = x. [resolve(58,a,55,b)]. 86 - Ex1At(A,x,W) | Enc(x,f4(x,c1)) | Enc(c1,f4(x,c1)) | c1 = x. [resolve(58,a,54,b)]. 94 - Ex1At(A,x,W) | Property(f4(x,c1)) | c1 = x. [resolve(58,a,50,b)]. 110 PartOf(c2,c2) | Enc(c2,f3(c2,c2)). [resolve(82,c,59,a),unit_del(a,57)]. 111 PartOf(c1,c1) | Enc(c1,f3(c1,c1)). [resolve(82,c,58,a),unit_del(a,56)]. 112 PartOf(c2,c2) | - Enc(c2,f3(c2,c2)). [resolve(83,c,59,a),unit_del(a,57)]. 113 PartOf(c1,c1) | - Enc(c1,f3(c1,c1)). [resolve(83,c,58,a),unit_del(a,56)]. 116 - Enc(c2,f4(c2,c1)) | - Enc(c1,f4(c2,c1)). [resolve(84,a,59,a),flip(c),unit_del(c,46)]. 123 PartOf(c2,c2). [resolve(112,b,110,b),merge(b)]. 124 PartOf(c2,c1). [back_unit_del(63),unit_del(b,123)]. 126 PartOf(c1,c1). [resolve(113,b,111,b),merge(b)]. 127 PartOf(c1,c2). [back_unit_del(60),unit_del(a,126)]. 128 Enc(c2,f4(c2,c1)) | Enc(c1,f4(c2,c1)). [resolve(86,a,59,a),flip(c),unit_del(c,46)]. 131 Enc(c1,f4(c2,c1)) | - Object(x) | - PartOf(c2,x) | - Property(f4(c2,c1)) | Enc(x,f4(c2,c1)). [resolve(128,a,49,e),unit_del(b,57)]. 132 Enc(c1,f4(c2,c1)) | - Property(f4(c2,c1)). [factor(131,a,e),unit_del(b,56),unit_del(c,124)]. 138 Property(f4(c2,c1)). [resolve(94,a,59,a),flip(b),unit_del(b,46)]. 139 Enc(c1,f4(c2,c1)). [back_unit_del(132),unit_del(b,138)]. 140 - Enc(c2,f4(c2,c1)). [back_unit_del(116),unit_del(b,139)]. 141 $F. [ur(49,a,56,a,b,57,a,c,127,a,d,138,a,f,140,a),unit_del(a,139)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=62. Generated=156. Kept=95. proofs=1. Usable=49. Sos=19. Demods=0. Denials=0. Limbo=0, Disabled=72. Hints=0. Megabytes=0.13. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3769 exit (max_proofs) Wed Jun 14 17:11:51 2006