============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3996 was started by zalta on mally, Wed Jun 14 17:54:20 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). assign(nest_penalty,10). assign(skolem_penalty,1). assign(max_weight,29). assign(max_vars,1). % formulas(usable). % not echoed (3 formulas) % formulas(sos). % not echoed (1 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <125,45>. Problem reduction (0.00 sec) gives one subproblem (<203,31>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 22 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 178.92 (+ 2.77) seconds. % Length of proof is 199. % Level of proof is 118. % Maximum clause weight is 29. % Given clauses 10438. 1 - Object(x) | - Object(y) | Object(f1(x,y)). [clausify]. 2 - Object(x) | - Object(y) | Ex1(A,f1(x,y),W). [clausify]. 3 - Object(x) | - Object(y) | - Property(z) | - Enc(f1(x,y),z) | Enc(x,z) | Enc(y,z). [clausify]. 4 - Object(x) | - Object(y) | - Property(z) | Enc(f1(x,y),z) | - Enc(x,z). [clausify]. 5 - Object(x) | - Object(y) | - Property(z) | Enc(f1(x,y),z) | - Enc(y,z). [clausify]. 9 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f2(x,y)). [clausify]. 10 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f2(x,y)). [clausify]. 11 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f2(x,y)). [clausify]. 12 - Object(x) | - Situation(x) | Ex1(A,x,W). [clausify]. 13 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)). [clausify]. 14 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y. [clausify]. 15 - Object(x) | Situation(x) | - Ex1(A,x,W) | Property(f4(x)). [clausify]. 16 - Object(x) | Situation(x) | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. 17 - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(y) | VAC(y) != f4(x). [clausify]. 23 - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(y) | f4(x) != VAC(y). [copy(17),flip(e)]. 24 Object(c1). [clausify]. 25 Object(c2). [clausify]. 26 Situation(c1). [clausify]. 27 Situation(c2). [clausify]. 28 - Object(x) | - Situation(x) | - PartOf(c1,x) | - PartOf(c2,x). [clausify]. 29 - Object(x) | Ex1(A,f1(x,c1),W). [resolve(24,a,2,b)]. 31 - Object(x) | Object(f1(x,c1)). [resolve(24,a,1,b)]. 37 Ex1(A,c1,W). [resolve(26,a,12,b),unit_del(a,24)]. 38 Ex1(A,c2,W). [resolve(27,a,12,b),unit_del(a,25)]. 39 Ex1(A,f1(c2,c1),W). [resolve(29,a,25,a)]. 42 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | - Enc(x,f2(c1,x)). [resolve(37,a,11,d),unit_del(a,24)]. 44 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Enc(c1,f2(c1,x)). [resolve(37,a,10,d),unit_del(a,24)]. 46 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Property(f2(c1,x)). [resolve(37,a,9,d),unit_del(a,24)]. 48 - Object(x) | PartOf(c2,x) | - Ex1(A,x,W) | - Enc(x,f2(c2,x)). [resolve(38,a,11,d),unit_del(a,25)]. 50 - Object(x) | PartOf(c2,x) | - Ex1(A,x,W) | Enc(c2,f2(c2,x)). [resolve(38,a,10,d),unit_del(a,25)]. 52 - Object(x) | PartOf(c2,x) | - Ex1(A,x,W) | Property(f2(c2,x)). [resolve(38,a,9,d),unit_del(a,25)]. 53 - Object(f1(c2,c1)) | Situation(f1(c2,c1)) | Enc(f1(c2,c1),f4(f1(c2,c1))). [resolve(39,a,16,c)]. 54 - Object(f1(c2,c1)) | Situation(f1(c2,c1)) | Property(f4(f1(c2,c1))). [resolve(39,a,15,c)]. 87 Object(f1(c2,c1)). [resolve(31,a,25,a)]. 98 Situation(f1(c2,c1)) | Property(f4(f1(c2,c1))). [back_unit_del(54),unit_del(a,87)]. 99 Situation(f1(c2,c1)) | Enc(f1(c2,c1),f4(f1(c2,c1))). [back_unit_del(53),unit_del(a,87)]. 183 Situation(f1(c2,c1)) | - Property(f4(f1(c2,c1))) | Enc(c2,f4(f1(c2,c1))) | Enc(c1,f4(f1(c2,c1))). [resolve(99,b,3,d),unit_del(b,25),unit_del(c,24)]. 199 PartOf(c1,f1(c2,c1)) | - Enc(f1(c2,c1),f2(c1,f1(c2,c1))). [resolve(42,c,39,a),unit_del(a,87)]. 220 PartOf(c1,f1(c2,c1)) | Enc(c1,f2(c1,f1(c2,c1))). [resolve(44,c,39,a),unit_del(a,87)]. 244 PartOf(c1,f1(c2,c1)) | Property(f2(c1,f1(c2,c1))). [resolve(46,c,39,a),unit_del(a,87)]. 271 PartOf(c2,f1(c2,c1)) | - Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [resolve(48,c,39,a),unit_del(a,87)]. 293 PartOf(c2,f1(c2,c1)) | Enc(c2,f2(c2,f1(c2,c1))). [resolve(50,c,39,a),unit_del(a,87)]. 315 PartOf(c2,f1(c2,c1)) | Property(f2(c2,f1(c2,c1))). [resolve(52,c,39,a),unit_del(a,87)]. 331 Enc(c2,f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)) | - PartOf(c1,f1(c2,c1)). [resolve(293,a,28,d),unit_del(b,87)]. 350 Property(f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)) | - PartOf(c1,f1(c2,c1)). [resolve(315,a,28,d),unit_del(b,87)]. 412 Enc(c2,f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)) | Property(f2(c1,f1(c2,c1))). [resolve(331,c,244,a)]. 413 Enc(c2,f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)) | Enc(c1,f2(c1,f1(c2,c1))). [resolve(331,c,220,a)]. 430 Property(f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)) | Property(f2(c1,f1(c2,c1))). [resolve(350,c,244,a)]. 431 Property(f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)) | Enc(c1,f2(c1,f1(c2,c1))). [resolve(350,c,220,a)]. 590 Enc(c2,f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(412,b,98,a)]. 591 Enc(c2,f2(c2,f1(c2,c1))) | Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(413,b,98,a)]. 620 Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(430,b,98,a)]. 621 Property(f2(c2,f1(c2,c1))) | Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(431,b,98,a)]. 715 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Object(x) | - Property(f2(c2,f1(c2,c1))) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(590,a,4,e),unit_del(c,25)]. 720 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Object(x) | - Property(f2(c2,f1(c2,c1))) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(591,a,4,e),unit_del(c,25)]. 742 Property(f2(c2,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Object(x) | - Property(f2(c1,f1(c2,c1))) | Enc(f1(x,c1),f2(c1,f1(c2,c1))). [resolve(621,b,5,e),unit_del(d,24)]. 1821 Situation(f1(c2,c1)) | Enc(c2,f4(f1(c2,c1))) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))). [resolve(183,b,620,c)]. 8296 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Property(f4(f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(1821,b,14,d),unit_del(e,25),unit_del(f,27)]. 8297 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Property(f4(f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(1821,b,13,d),unit_del(e,25),unit_del(f,27)]. 20375 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(8297,e,620,c),merge(f),merge(g)]. 20380 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(20375,b,14,d),unit_del(e,24),unit_del(f,26)]. 20381 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(20375,b,13,d),unit_del(e,24),unit_del(f,26)]. 24108 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(8296,e,620,c),merge(f),merge(g)]. 24142 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c2,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(24108(e,1),23(e,2)),flip(i)]. 24143 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Proposition(f3(c2,f4(f1(c2,c1)))). [factor(24142,a,f),xx(h),unit_del(e,87),unit_del(f,39)]. 24520 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(20381,e,620,c),merge(f),merge(g)]. 24521 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))) | Enc(c1,f4(f1(c2,c1))). [resolve(24520,d,24143,e),merge(e),merge(g),merge(h)]. 24527 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))). [resolve(24521,e,13,d),merge(h),unit_del(e,24),unit_del(f,26)]. 24528 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(24527,e,620,c),merge(e),merge(f)]. 31870 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(20380,e,620,c),merge(f),merge(g)]. 31871 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(31870(e,1),23(e,2)),flip(i)]. 31872 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(31871,a,f),xx(h),unit_del(e,87),unit_del(f,39)]. 31874 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(31872,e,24528,d),merge(e),merge(f),merge(g)]. 31875 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | Enc(c1,f4(f1(c2,c1))). [resolve(31874,d,24143,e),merge(d),merge(f),merge(g)]. 31880 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Property(f4(f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(31875,d,14,d),unit_del(d,24),unit_del(e,26)]. 31902 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(31880,d,620,c),merge(e),merge(f)]. 31903 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(31902(d,1),23(e,2)),flip(h)]. 31904 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(31903,a,e),xx(g),unit_del(d,87),unit_del(e,39)]. 31905 Situation(f1(c2,c1)) | Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))). [resolve(31904,d,24528,d),merge(d),merge(e),merge(f)]. 32214 Property(f2(c2,f1(c2,c1))) | Property(f2(c1,f1(c2,c1))). [resolve(31905,a,430,b),merge(c),merge(d)]. 32225 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Object(x) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(32214,a,715,d),merge(b)]. 32280 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [resolve(32225,c,24,a)]. 32294 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | PartOf(c2,f1(c2,c1)). [resolve(32280,c,271,b)]. 32299 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)) | - PartOf(c1,f1(c2,c1)). [resolve(32294,c,28,d),unit_del(c,87)]. 32301 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(32299,d,244,a),merge(d)]. 32303 Property(f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(32301,c,98,a),merge(c)]. 32308 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c2,f4(f1(c2,c1))) | Enc(c1,f4(f1(c2,c1))). [resolve(32303,b,183,b)]. 32317 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Property(f4(f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(32308,c,14,d),unit_del(d,25),unit_del(e,27)]. 32318 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Property(f4(f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(32308,c,13,d),unit_del(d,25),unit_del(e,27)]. 32479 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(32318,d,32303,b),merge(e)]. 32484 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(32479,c,14,d),unit_del(d,24),unit_del(e,26)]. 32485 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(32479,c,13,d),unit_del(d,24),unit_del(e,26)]. 32537 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(32485,d,32303,b),merge(e)]. 32844 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(32317,d,32303,b),merge(e)]. 32845 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c2,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(32844(d,1),23(e,2)),flip(h)]. 32846 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Proposition(f3(c2,f4(f1(c2,c1)))). [factor(32845,b,e),xx(g),unit_del(d,87),unit_del(e,39)]. 32848 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(32846,d,32537,c),merge(d),merge(e)]. 32854 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c1,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))). [resolve(32848,c,13,d),merge(g),unit_del(d,24),unit_del(e,26)]. 32855 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(32854,d,32303,b),merge(d)]. 33160 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(32484,d,32303,b),merge(e)]. 33161 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(33160(d,1),23(e,2)),flip(h)]. 33162 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(33161,b,e),xx(g),unit_del(d,87),unit_del(e,39)]. 33163 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(33162,d,32855,c),merge(d),merge(e)]. 33164 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))). [resolve(33163,c,32846,d),merge(c),merge(d)]. 33169 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | - Property(f4(f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(33164,c,14,d),unit_del(c,24),unit_del(d,26)]. 33199 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(33169,c,32303,b),merge(d)]. 33200 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(33199(c,1),23(e,2)),flip(g)]. 33201 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(33200,b,d),xx(f),unit_del(c,87),unit_del(d,39)]. 33203 Property(f2(c1,f1(c2,c1))) | Situation(f1(c2,c1)). [resolve(33201,c,32855,c),merge(c),merge(d)]. 33527 Property(f2(c1,f1(c2,c1))) | Enc(c2,f2(c2,f1(c2,c1))). [resolve(33203,b,412,b),merge(c)]. 33539 Property(f2(c1,f1(c2,c1))) | - Object(x) | - Property(f2(c2,f1(c2,c1))) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(33527,b,4,e),unit_del(b,25)]. 33975 Property(f2(c1,f1(c2,c1))) | - Object(x) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(33539,c,32214,a),merge(d)]. 33996 Property(f2(c1,f1(c2,c1))) | Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [resolve(33975,b,24,a)]. 34001 Property(f2(c1,f1(c2,c1))) | PartOf(c2,f1(c2,c1)). [resolve(33996,b,271,b)]. 34006 Property(f2(c1,f1(c2,c1))) | - Situation(f1(c2,c1)) | - PartOf(c1,f1(c2,c1)). [resolve(34001,b,28,d),unit_del(b,87)]. 34008 Property(f2(c1,f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(34006,c,244,a),merge(c)]. 34009 Property(f2(c1,f1(c2,c1))). [resolve(34008,b,33203,b),merge(b)]. 34015 Property(f2(c2,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Object(x) | Enc(f1(x,c1),f2(c1,f1(c2,c1))). [back_unit_del(742),unit_del(d,34009)]. 34071 Property(f2(c2,f1(c2,c1))) | Property(f4(f1(c2,c1))) | Enc(f1(c2,c1),f2(c1,f1(c2,c1))). [resolve(34015,c,25,a)]. 34072 Property(f2(c2,f1(c2,c1))) | Property(f4(f1(c2,c1))) | PartOf(c1,f1(c2,c1)). [resolve(34071,c,199,b)]. 34077 Property(f2(c2,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(34072,c,350,c),merge(c)]. 34079 Property(f2(c2,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(34077,c,98,a),merge(c)]. 34084 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c2,f4(f1(c2,c1))) | Enc(c1,f4(f1(c2,c1))). [resolve(34079,b,183,b)]. 34093 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Property(f4(f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(34084,c,14,d),unit_del(d,25),unit_del(e,27)]. 34094 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Property(f4(f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(34084,c,13,d),unit_del(d,25),unit_del(e,27)]. 34250 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(34094,d,34079,b),merge(e)]. 34255 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(34250,c,14,d),unit_del(d,24),unit_del(e,26)]. 34256 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(34250,c,13,d),unit_del(d,24),unit_del(e,26)]. 34310 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(34256,d,34079,b),merge(e)]. 34567 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(34093,d,34079,b),merge(e)]. 34568 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c2,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(34567(d,1),23(e,2)),flip(h)]. 34569 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Proposition(f3(c2,f4(f1(c2,c1)))). [factor(34568,b,e),xx(g),unit_del(d,87),unit_del(e,39)]. 34570 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(34569,d,34310,c),merge(d),merge(e)]. 34576 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c1,f4(f1(c2,c1)))) | - Property(f4(f1(c2,c1))). [resolve(34570,c,13,d),merge(g),unit_del(d,24),unit_del(e,26)]. 34577 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(34576,d,34079,b),merge(d)]. 34846 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(34255,d,34079,b),merge(e)]. 34847 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(34846(d,1),23(e,2)),flip(h)]. 34848 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(34847,b,e),xx(g),unit_del(d,87),unit_del(e,39)]. 34849 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(34848,d,34577,c),merge(d),merge(e)]. 34850 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))). [resolve(34849,c,34569,d),merge(c),merge(d)]. 34855 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | - Property(f4(f1(c2,c1))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(34850,c,14,d),unit_del(c,24),unit_del(d,26)]. 34886 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(34855,c,34079,b),merge(d)]. 34887 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(34886(c,1),23(e,2)),flip(g)]. 34888 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(34887,b,d),xx(f),unit_del(c,87),unit_del(d,39)]. 34889 Property(f2(c2,f1(c2,c1))) | Situation(f1(c2,c1)). [resolve(34888,c,34577,c),merge(c),merge(d)]. 35222 Property(f2(c2,f1(c2,c1))) | Enc(c1,f2(c1,f1(c2,c1))). [resolve(34889,b,431,b),merge(b)]. 35231 Property(f2(c2,f1(c2,c1))) | - Object(x) | Enc(f1(x,c1),f2(c1,f1(c2,c1))). [resolve(35222,b,5,e),unit_del(c,24),unit_del(d,34009)]. 35305 Property(f2(c2,f1(c2,c1))) | Enc(f1(c2,c1),f2(c1,f1(c2,c1))). [resolve(35231,b,25,a)]. 35309 Property(f2(c2,f1(c2,c1))) | PartOf(c1,f1(c2,c1)). [resolve(35305,b,199,b)]. 35314 Property(f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(35309,b,350,c),merge(b)]. 35316 Property(f2(c2,f1(c2,c1))). [resolve(35314,b,34889,b),merge(b)]. 35322 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Object(x) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [back_unit_del(720),unit_del(d,35316)]. 35403 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [resolve(35322,c,24,a)]. 35416 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | PartOf(c2,f1(c2,c1)). [resolve(35403,c,271,b)]. 35422 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)) | - PartOf(c1,f1(c2,c1)). [resolve(35416,c,28,d),unit_del(c,87)]. 35424 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(35422,d,220,a),merge(d)]. 35425 Enc(c1,f2(c1,f1(c2,c1))) | Property(f4(f1(c2,c1))). [resolve(35424,c,98,a),merge(c)]. 35432 Property(f4(f1(c2,c1))) | - Object(x) | Enc(f1(x,c1),f2(c1,f1(c2,c1))). [resolve(35425,a,5,e),unit_del(c,24),unit_del(d,34009)]. 35485 Property(f4(f1(c2,c1))) | Enc(f1(c2,c1),f2(c1,f1(c2,c1))). [resolve(35432,b,25,a)]. 35489 Property(f4(f1(c2,c1))) | PartOf(c1,f1(c2,c1)). [resolve(35485,b,199,b)]. 35494 Property(f4(f1(c2,c1))) | Enc(c2,f2(c2,f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(35489,b,331,c)]. 35502 Property(f4(f1(c2,c1))) | Enc(c2,f2(c2,f1(c2,c1))). [resolve(35494,c,98,a),merge(c)]. 35512 Property(f4(f1(c2,c1))) | - Object(x) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(35502,b,4,e),unit_del(b,25),unit_del(d,35316)]. 35681 Property(f4(f1(c2,c1))) | Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [resolve(35512,b,24,a)]. 35684 Property(f4(f1(c2,c1))) | PartOf(c2,f1(c2,c1)). [resolve(35681,b,271,b)]. 35689 Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)) | - PartOf(c1,f1(c2,c1)). [resolve(35684,b,28,d),unit_del(b,87)]. 35691 Property(f4(f1(c2,c1))) | - Situation(f1(c2,c1)). [resolve(35689,c,35489,b),merge(c)]. 35692 Property(f4(f1(c2,c1))). [resolve(35691,b,98,a),merge(b)]. 35697 Situation(f1(c2,c1)) | Enc(c2,f4(f1(c2,c1))) | Enc(c1,f4(f1(c2,c1))). [back_unit_del(183),unit_del(b,35692)]. 35706 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | VAC(f3(c2,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(35697,b,14,d),unit_del(c,25),unit_del(d,27),unit_del(e,35692)]. 35707 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(35697,b,13,d),unit_del(c,25),unit_del(d,27),unit_del(e,35692)]. 35729 Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(35707,b,14,d),unit_del(c,24),unit_del(d,26),unit_del(e,35692)]. 35730 Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(35707,b,13,d),unit_del(c,24),unit_del(d,26),unit_del(e,35692)]. 35923 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c2,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(35706(c,1),23(e,2)),flip(g)]. 35924 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | - Proposition(f3(c2,f4(f1(c2,c1)))). [factor(35923,a,d),xx(f),unit_del(c,87),unit_del(d,39)]. 35925 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(35924,c,35730,b),merge(c)]. 35931 Situation(f1(c2,c1)) | Proposition(f3(c1,f4(f1(c2,c1)))). [resolve(35925,b,13,d),merge(f),unit_del(c,24),unit_del(d,26),unit_del(e,35692)]. 36127 Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(35729(c,1),23(e,2)),flip(g)]. 36128 Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(36127,a,d),xx(f),unit_del(c,87),unit_del(d,39)]. 36129 Situation(f1(c2,c1)) | Proposition(f3(c2,f4(f1(c2,c1)))). [resolve(36128,c,35931,b),merge(c)]. 36130 Situation(f1(c2,c1)) | Enc(c1,f4(f1(c2,c1))). [resolve(36129,b,35924,c),merge(b)]. 36135 Situation(f1(c2,c1)) | VAC(f3(c1,f4(f1(c2,c1)))) = f4(f1(c2,c1)). [resolve(36130,b,14,d),unit_del(b,24),unit_del(c,26),unit_del(d,35692)]. 36160 Situation(f1(c2,c1)) | - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(f3(c1,f4(f1(c2,c1)))) | f4(f1(c2,c1)) != f4(x). [para(36135(b,1),23(e,2)),flip(f)]. 36161 Situation(f1(c2,c1)) | - Proposition(f3(c1,f4(f1(c2,c1)))). [factor(36160,a,c),xx(e),unit_del(b,87),unit_del(c,39)]. 36163 Situation(f1(c2,c1)). [resolve(36161,b,35931,b),merge(b)]. 36860 Enc(c2,f2(c2,f1(c2,c1))) | Enc(c1,f2(c1,f1(c2,c1))). [back_unit_del(413),unit_del(b,36163)]. 36863 Enc(c2,f2(c2,f1(c2,c1))) | - PartOf(c1,f1(c2,c1)). [back_unit_del(331),unit_del(b,36163)]. 36885 Enc(c1,f2(c1,f1(c2,c1))) | - Object(x) | Enc(f1(c2,x),f2(c2,f1(c2,c1))). [resolve(36860,a,4,e),unit_del(b,25),unit_del(d,35316)]. 37193 Enc(c1,f2(c1,f1(c2,c1))) | Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [resolve(36885,b,24,a)]. 37196 Enc(c1,f2(c1,f1(c2,c1))) | PartOf(c2,f1(c2,c1)). [resolve(37193,b,271,b)]. 37201 Enc(c1,f2(c1,f1(c2,c1))) | - PartOf(c1,f1(c2,c1)). [resolve(37196,b,28,d),unit_del(b,87),unit_del(c,36163)]. 37204 Enc(c1,f2(c1,f1(c2,c1))). [resolve(37201,b,220,a),merge(b)]. 37211 - Object(x) | Enc(f1(x,c1),f2(c1,f1(c2,c1))). [resolve(37204,a,5,e),unit_del(b,24),unit_del(c,34009)]. 37265 Enc(f1(c2,c1),f2(c1,f1(c2,c1))). [resolve(37211,a,25,a)]. 37267 PartOf(c1,f1(c2,c1)). [back_unit_del(199),unit_del(b,37265)]. 37268 Enc(c2,f2(c2,f1(c2,c1))). [back_unit_del(36863),unit_del(b,37267)]. 37270 - PartOf(c2,f1(c2,c1)). [ur(28,a,87,a,b,36163,a,c,37267,a)]. 37271 - Enc(f1(c2,c1),f2(c2,f1(c2,c1))). [back_unit_del(271),unit_del(a,37270)]. 37289 $F. [ur(4,b,24,a,c,35316,a,d,37271,a,e,37268,a),unit_del(a,25)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=10438. Generated=182551. Kept=37265. proofs=1. Usable=4426. Sos=3187. Demods=19. Denials=0. Limbo=1, Disabled=29674. Hints=0. Megabytes=17.72. User_CPU=178.92, System_CPU=2.77, Wall_clock=184. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3996 exit (max_proofs) Wed Jun 14 17:57:24 2006