============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3770 was started by zalta on mally, Wed Jun 14 17:11:55 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(quiet). set(print_given). % formulas(sos). % not echoed (5 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <135,98>. Problem reduction (0.00 sec) gives 3 independent subproblems: ( <181,33> <186,36> <189,37> ). Max nnf_size of subproblems is 189; max cnf_max is 37. ============================== FOF REDUCTION MULTISEARCH ============= Starting Subproblem 1 of 3. Child search process 3771 started. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 33 clauses. Predicate elimination: Situation/1. Term ordering decisions: Relation symbol precedence: lex([ Object, Property, Proposition, Enc, PartOf, Ex1, =, Situation ]). Function symbol precedence: lex([ A, W, c1, f2, f3, f5, f6, f7, f8, VAC, f1, f4 ]). After inverse_order: Function symbol precedence: lex([ A, W, c1, f2, f3, f5, f6, f7, f8, VAC, f1, f4 ]). Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (less than 100 clauses) Reasonable options, based on the structure of the clauses: % set(factor), because non-Horn % set(back_unit_deletion), because non-Horn % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=1): 44 - PartOf(c1,c1). [clausify]. given #2 (I,wt=11): 45 - Object(x) | Ex1(A,x,W) | - Object(y) | - PartOf(x,y). [clausify]. given #3 (I,wt=11): 46 - Object(x) | - Object(y) | Ex1(A,y,W) | - PartOf(x,y). [clausify]. given #4 (I,wt=15): 47 - Object(x) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - PartOf(x,y). [clausify]. given #5 (I,wt=18): 48 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | Property(f4(x)). [clausify]. given #6 (I,wt=19): 49 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. given #7 (I,wt=19): 50 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Property(f5(x,y)). [clausify]. given #8 (I,wt=19): 51 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #9 (I,wt=20): 52 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | Property(f4(x)). [clausify]. given #10 (I,wt=20): 53 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Enc(x,f5(x,y)). [clausify]. given #11 (I,wt=20): 54 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | - Enc(y,f5(x,y)). [clausify]. given #12 (I,wt=20): 55 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #13 (I,wt=20): 56 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #14 (I,wt=20): 57 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #15 (I,wt=20): 58 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #16 (I,wt=21): 59 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. given #17 (I,wt=21): 60 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #18 (I,wt=21): 61 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #19 (I,wt=21): 62 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #20 (I,wt=21): 63 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #21 (I,wt=22): 64 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | - Proposition(z) | f4(x) != VAC(z). [copy(29),flip(g)]. given #22 (I,wt=24): 65 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | - Proposition(z) | f4(x) != VAC(z). [copy(30),flip(g)]. given #23 (I,wt=24): 66 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | Property(f6(x,y)). [clausify]. given #24 (I,wt=25): 67 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | Enc(x,f6(x,y)). [clausify]. given #25 (I,wt=25): 68 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | - Enc(y,f6(x,y)). [clausify]. given #26 (I,wt=1): 69 Object(c1). [resolve(3,a,1,a)]. given #27 (I,wt=3): 70 Ex1(A,c1,W). [copy(35),unit_del(a,69)]. given #28 (I,wt=7): 71 - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [copy(36),unit_del(a,69)]. given #29 (I,wt=18): 72 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)) | - Ex1(A,x,W) | Property(f1(x)). [copy(37),merge(e)]. given #30 (I,wt=19): 73 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)) | - Ex1(A,x,W) | Enc(x,f1(x)). [copy(38),merge(e)]. given #31 (I,wt=22): 74 - Object(x) | - Ex1(A,x,W) | - Proposition(y) | f1(x) != VAC(y) | - Property(z) | - Enc(x,z) | Proposition(f2(x,z)). [copy(39),flip(d),merge(e)]. given #32 (I,wt=9): 75 - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [copy(40),unit_del(a,69)]. given #33 (I,wt=20): 76 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | Property(f1(x)). [copy(41),merge(e)]. given #34 (I,wt=21): 77 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | Enc(x,f1(x)). [copy(42),merge(e)]. given #35 (I,wt=24): 78 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | - Proposition(z) | f1(x) != VAC(z). [copy(43),flip(h),merge(e)]. given #36 (I,wt=9): 79 - Object(x) | Ex1(A,x,W) | - PartOf(x,x). [factor(45,a,c)]. given #37 (I,wt=13): 80 - Object(x) | - Ex1(A,x,W) | PartOf(x,x) | Property(f5(x,x)). [factor(50,a,c),merge(d)]. given #38 (I,wt=14): 81 - Object(x) | - Ex1(A,x,W) | PartOf(x,x) | Enc(x,f5(x,x)). [factor(53,a,c),merge(d)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 12. % Level of proof is 4. % Maximum clause weight is 20. % Given clauses 38. 1 Situation(c1). [clausify]. 3 - Situation(x) | Object(x). [clausify]. 4 - Object(x) | Ex1(A,x,W) | - Situation(x). [clausify]. 35 - Object(c1) | Ex1(A,c1,W). [resolve(4,c,1,a)]. 44 - PartOf(c1,c1). [clausify]. 53 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Enc(x,f5(x,y)). [clausify]. 54 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | - Enc(y,f5(x,y)). [clausify]. 69 Object(c1). [resolve(3,a,1,a)]. 70 Ex1(A,c1,W). [copy(35),unit_del(a,69)]. 81 - Object(x) | - Ex1(A,x,W) | PartOf(x,x) | Enc(x,f5(x,x)). [factor(53,a,c),merge(d)]. 117 - Enc(c1,f5(c1,c1)). [ur(54,a,69,a,b,70,a,c,69,a,d,44,a,e,70,a)]. 119 $F. [resolve(81,b,70,a),unit_del(a,69),unit_del(b,44),unit_del(c,117)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=38. Generated=107. Kept=75. proofs=1. Usable=38. Sos=37. Demods=0. Denials=0. Limbo=0, Disabled=43. Hints=0. Megabytes=0.18. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3771 exit (max_proofs) Wed Jun 14 17:11:55 2006 ============================== continuing FOF reduction multisearch == Starting Subproblem 2 of 3. Child search process 3772 started. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 36 clauses. Predicate elimination: Situation/1 PartOf/2. Term ordering decisions: Relation symbol precedence: lex([ Object, Property, Proposition, Enc, Ex1, =, PartOf, Situation ]). Function symbol precedence: lex([ A, W, c1, c2, f2, f3, f5, f6, f7, f8, VAC, f1, f4 ]). After inverse_order: Function symbol precedence: lex([ A, W, c1, c2, f2, f3, f5, f6, f7, f8, VAC, f1, f4 ]). Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (less than 100 clauses) Reasonable options, based on the structure of the clauses: % set(factor), because non-Horn % set(back_unit_deletion), because non-Horn % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=1): 60 c2 != c1. [clausify]. given #2 (I,wt=18): 61 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | Property(f4(x)). [clausify]. given #3 (I,wt=19): 62 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. given #4 (I,wt=19): 63 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #5 (I,wt=20): 64 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | Property(f4(x)). [clausify]. given #6 (I,wt=20): 65 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #7 (I,wt=20): 66 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #8 (I,wt=20): 67 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #9 (I,wt=20): 68 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #10 (I,wt=21): 69 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. given #11 (I,wt=21): 70 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #12 (I,wt=21): 71 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #13 (I,wt=21): 72 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #14 (I,wt=21): 73 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #15 (I,wt=22): 74 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | - Proposition(z) | f4(x) != VAC(z). [copy(32),flip(g)]. given #16 (I,wt=24): 75 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | - Proposition(z) | f4(x) != VAC(z). [copy(33),flip(g)]. given #17 (I,wt=24): 76 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | Property(f6(x,y)). [clausify]. given #18 (I,wt=25): 77 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | Enc(x,f6(x,y)). [clausify]. given #19 (I,wt=25): 78 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | - Enc(y,f6(x,y)). [clausify]. given #20 (I,wt=1): 79 Object(c1). [resolve(6,a,1,a)]. given #21 (I,wt=1): 80 Object(c2). [resolve(6,a,2,a)]. given #22 (I,wt=3): 81 Ex1(A,c1,W). [copy(39),unit_del(a,79)]. given #23 (I,wt=3): 82 Ex1(A,c2,W). [copy(40),unit_del(a,80)]. given #24 (I,wt=7): 83 - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [copy(41),unit_del(a,79)]. given #25 (I,wt=7): 84 - Property(x) | - Enc(c2,x) | Proposition(f2(c2,x)). [copy(42),unit_del(a,80)]. given #26 (I,wt=18): 85 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)) | - Ex1(A,x,W) | Property(f1(x)). [copy(43),merge(e)]. given #27 (I,wt=19): 86 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)) | - Ex1(A,x,W) | Enc(x,f1(x)). [copy(44),merge(e)]. given #28 (I,wt=22): 87 - Object(x) | - Ex1(A,x,W) | - Proposition(y) | f1(x) != VAC(y) | - Property(z) | - Enc(x,z) | Proposition(f2(x,z)). [copy(45),flip(d),merge(e)]. given #29 (I,wt=9): 88 - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [copy(46),unit_del(a,79)]. given #30 (I,wt=9): 89 - Property(x) | - Enc(c2,x) | VAC(f2(c2,x)) = x. [copy(47),unit_del(a,80)]. given #31 (I,wt=20): 90 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | Property(f1(x)). [copy(48),merge(e)]. given #32 (I,wt=21): 91 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | Enc(x,f1(x)). [copy(49),merge(e)]. given #33 (I,wt=24): 92 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | - Proposition(z) | f1(x) != VAC(z). [copy(50),flip(h),merge(e)]. given #34 (I,wt=6): 93 - Property(x) | - Enc(c1,x) | Enc(c2,x). [copy(55),unit_del(a,79),unit_del(b,80)]. given #35 (I,wt=6): 94 - Property(x) | - Enc(c2,x) | Enc(c1,x). [copy(56),unit_del(a,80),unit_del(b,79)]. given #36 (I,wt=24): 95 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Ex1(A,y,W) | Property(f5(x,y)) | - Property(z) | - Enc(x,z) | Enc(y,z). [copy(57),merge(f),merge(g)]. given #37 (I,wt=25): 96 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Ex1(A,y,W) | Enc(x,f5(x,y)) | - Property(z) | - Enc(x,z) | Enc(y,z). [copy(58),merge(f),merge(g)]. given #38 (I,wt=25): 97 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Ex1(A,y,W) | - Enc(y,f5(x,y)) | - Property(z) | - Enc(x,z) | Enc(y,z). [copy(59),merge(f),merge(g)]. given #39 (T,wt=9): 124 - Property(x) | - Enc(c1,x) | Proposition(f3(c1,x)) | Enc(c1,f4(c1)). [resolve(81,a,62,e),unit_del(a,79)]. given #40 (T,wt=9): 125 - Property(x) | - Enc(c1,x) | Proposition(f3(c1,x)) | Property(f4(c1)). [resolve(81,a,61,e),unit_del(a,79)]. given #41 (A,wt=16): 98 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c1,y) | - Enc(c1,f6(x,c1)). [resolve(81,a,78,g),unit_del(c,79)]. given #42 (F,wt=9): 152 - Property(x) | - Enc(c2,x) | Proposition(f3(c2,x)) | Enc(c2,f4(c2)). [resolve(82,a,62,e),unit_del(a,80)]. given #43 (F,wt=9): 153 - Property(x) | - Enc(c2,x) | Proposition(f3(c2,x)) | Property(f4(c2)). [resolve(82,a,61,e),unit_del(a,80)]. given #44 (T,wt=11): 112 - Property(x) | - Enc(c1,x) | VAC(f3(c1,x)) = x | Enc(c1,f4(c1)). [resolve(81,a,69,e),unit_del(a,79)]. given #45 (T,wt=11): 121 - Property(x) | - Enc(c1,x) | VAC(f3(c1,x)) = x | Property(f4(c1)). [resolve(81,a,64,e),unit_del(a,79)]. given #46 (A,wt=17): 99 - Object(x) | - Property(y) | - Enc(c1,y) | Enc(x,y) | - Ex1(A,x,W) | - Enc(x,f6(c1,x)). [resolve(81,a,78,b),unit_del(a,79)]. given #47 (F,wt=11): 140 - Property(x) | - Enc(c2,x) | VAC(f3(c2,x)) = x | Enc(c2,f4(c2)). [resolve(82,a,69,e),unit_del(a,80)]. given #48 (F,wt=11): 149 - Property(x) | - Enc(c2,x) | VAC(f3(c2,x)) = x | Property(f4(c2)). [resolve(82,a,64,e),unit_del(a,80)]. given #49 (T,wt=12): 104 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(81,a,73,b)]. given #50 (T,wt=4): 166 - Enc(c1,f7(c2,c1)) | Enc(c1,f8(c2,c1)). [resolve(104,a,82,a),flip(c),unit_del(c,60)]. % SOS Control: given=50, spent=0/3000 (ticks), new_sos_limit=2147483647, disabled=0, user_seconds=0.01. given #51 (A,wt=17): 100 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c1,y) | Enc(x,f6(x,c1)). [resolve(81,a,77,g),unit_del(c,79)]. given #52 (F,wt=12): 111 - Ex1(A,x,W) | Enc(c1,f7(c1,x)) | - Enc(c1,f8(c1,x)) | c1 = x. [resolve(81,a,70,a),flip(d)]. given #53 (F,wt=4): 167 Enc(c1,f7(c1,c2)) | - Enc(c1,f8(c1,c2)). [resolve(111,a,82,a),flip(c),unit_del(c,60)]. given #54 (T,wt=12): 113 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(81,a,68,b)]. given #55 (T,wt=4): 168 - Enc(c1,f7(c2,c1)) | Property(f8(c2,c1)). [resolve(113,a,82,a),flip(c),unit_del(c,60)]. given #56 (A,wt=16): 101 - Object(x) | - Property(y) | - Enc(c1,y) | Enc(x,y) | - Ex1(A,x,W) | Enc(c1,f6(c1,x)). [resolve(81,a,77,b),unit_del(a,79)]. given #57 (F,wt=12): 116 - Ex1(A,x,W) | Enc(c1,f7(c1,x)) | Property(f8(c1,x)) | c1 = x. [resolve(81,a,67,a),flip(d)]. given #58 (F,wt=4): 169 Enc(c1,f7(c1,c2)) | Property(f8(c1,c2)). [resolve(116,a,82,a),flip(c),unit_del(c,60)]. given #59 (T,wt=6): 174 Property(f8(c1,c2)) | - Property(f7(c1,c2)) | Enc(c2,f7(c1,c2)). [resolve(169,a,93,b)]. given #60 (T,wt=9): 176 Property(f8(c1,c2)) | - Property(f7(c1,c2)) | Proposition(f2(c1,f7(c1,c2))). [resolve(169,a,83,b)]. given #61 (A,wt=16): 102 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c1,y) | Property(f6(x,c1)). [resolve(81,a,76,g),unit_del(c,79)]. given #62 (F,wt=11): 170 Property(f8(c1,c2)) | - Property(f7(c1,c2)) | Proposition(f3(c1,f7(c1,c2))) | Property(f4(c1)). [resolve(169,a,125,b)]. given #63 (F,wt=11): 171 Property(f8(c1,c2)) | - Property(f7(c1,c2)) | Proposition(f3(c1,f7(c1,c2))) | Enc(c1,f4(c1)). [resolve(169,a,124,b)]. given #64 (T,wt=11): 175 Property(f8(c1,c2)) | - Property(f7(c1,c2)) | VAC(f2(c1,f7(c1,c2))) = f7(c1,c2). [resolve(169,a,88,b)]. given #65 (T,wt=12): 117 - Ex1(A,x,W) | Property(f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(81,a,66,b)]. given #66 (A,wt=16): 103 - Object(x) | - Property(y) | - Enc(c1,y) | Enc(x,y) | - Ex1(A,x,W) | Property(f6(c1,x)). [resolve(81,a,76,b),unit_del(a,79)]. given #67 (F,wt=4): 177 Property(f7(c2,c1)) | Enc(c1,f8(c2,c1)). [resolve(117,a,82,a),flip(c),unit_del(c,60)]. given #68 (F,wt=6): 182 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(177,b,93,b)]. given #69 (T,wt=9): 184 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Proposition(f2(c1,f8(c2,c1))). [resolve(177,b,83,b)]. given #70 (T,wt=11): 178 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Proposition(f3(c1,f8(c2,c1))) | Property(f4(c1)). [resolve(177,b,125,b)]. given #71 (A,wt=14): 105 - Ex1(A,x,W) | - Enc(x,f7(c1,x)) | Enc(x,f8(c1,x)) | c1 = x. [resolve(81,a,73,a),flip(d)]. given #72 (F,wt=4): 185 - Enc(c2,f7(c1,c2)) | Enc(c2,f8(c1,c2)). [resolve(105,a,82,a),flip(c),unit_del(c,60)]. given #73 (F,wt=11): 179 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Proposition(f3(c1,f8(c2,c1))) | Enc(c1,f4(c1)). [resolve(177,b,124,b)]. given #74 (T,wt=11): 183 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | VAC(f2(c1,f8(c2,c1))) = f8(c2,c1). [resolve(177,b,88,b)]. given #75 (T,wt=12): 120 - Ex1(A,x,W) | Property(f7(c1,x)) | - Enc(c1,f8(c1,x)) | c1 = x. [resolve(81,a,65,a),flip(d)]. given #76 (A,wt=13): 106 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(81,a,72,b)]. given #77 (F,wt=4): 187 - Enc(c1,f7(c2,c1)) | - Enc(c2,f8(c2,c1)). [resolve(106,a,82,a),flip(c),unit_del(c,60)]. given #78 (F,wt=4): 186 Property(f7(c1,c2)) | - Enc(c1,f8(c1,c2)). [resolve(120,a,82,a),flip(c),unit_del(c,60)]. given #79 (T,wt=12): 122 - Ex1(A,x,W) | Property(f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(81,a,63,b)]. given #80 (T,wt=4): 188 Property(f7(c2,c1)) | Property(f8(c2,c1)). [resolve(122,a,82,a),flip(c),unit_del(c,60)]. given #81 (A,wt=13): 107 - Ex1(A,x,W) | - Enc(x,f7(c1,x)) | - Enc(c1,f8(c1,x)) | c1 = x. [resolve(81,a,72,a),flip(d)]. given #82 (F,wt=4): 194 - Enc(c2,f7(c1,c2)) | - Enc(c1,f8(c1,c2)). [resolve(107,a,82,a),flip(c),unit_del(c,60)]. given #83 (F,wt=4): 191 Property(f7(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(188,b,182,b),merge(b)]. given #84 (T,wt=4): 195 Property(f7(c2,c1)) | - Enc(c1,f7(c2,c1)). [resolve(191,b,187,b)]. given #85 (T,wt=7): 189 Property(f7(c2,c1)) | Proposition(f2(c1,f8(c2,c1))). [resolve(188,b,184,b),merge(b)]. given #86 (A,wt=13): 108 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(81,a,71,b)]. given #87 (F,wt=4): 202 Enc(c2,f7(c2,c1)) | Enc(c1,f8(c2,c1)). [resolve(108,a,82,a),flip(c),unit_del(c,60)]. given #88 (F,wt=6): 207 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)). [resolve(202,a,94,b)]. given #89 (T,wt=9): 190 Property(f7(c2,c1)) | VAC(f2(c1,f8(c2,c1))) = f8(c2,c1). [resolve(188,b,183,b),merge(b)]. given #90 (T,wt=9): 192 Property(f7(c2,c1)) | Proposition(f3(c1,f8(c2,c1))) | Enc(c1,f4(c1)). [resolve(188,b,179,b),merge(b)]. given #91 (A,wt=13): 109 - Ex1(A,x,W) | Enc(c1,f7(c1,x)) | Enc(x,f8(c1,x)) | c1 = x. [resolve(81,a,71,a),flip(d)]. given #92 (F,wt=4): 217 Enc(c1,f7(c1,c2)) | Enc(c2,f8(c1,c2)). [resolve(109,a,82,a),flip(c),unit_del(c,60)]. given #93 (F,wt=6): 222 Enc(c1,f7(c1,c2)) | - Property(f8(c1,c2)) | Enc(c1,f8(c1,c2)). [resolve(217,b,94,b)]. given #94 (T,wt=9): 193 Property(f7(c2,c1)) | Proposition(f3(c1,f8(c2,c1))) | Property(f4(c1)). [resolve(188,b,178,b),merge(b)]. given #95 (T,wt=9): 201 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Proposition(f2(c2,f8(c2,c1))). [resolve(191,b,84,b)]. given #96 (A,wt=14): 110 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(81,a,70,b)]. given #97 (F,wt=4): 226 Enc(c2,f7(c2,c1)) | - Enc(c2,f8(c2,c1)). [resolve(110,a,82,a),flip(c),unit_del(c,60)]. given #98 (F,wt=4): 227 Enc(c2,f7(c2,c1)) | Property(f7(c2,c1)). [resolve(226,b,191,b)]. given #99 (T,wt=7): 225 Property(f7(c2,c1)) | Proposition(f2(c2,f8(c2,c1))). [resolve(201,b,188,b),merge(c)]. given #100 (T,wt=9): 209 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Proposition(f2(c2,f7(c2,c1))). [resolve(202,a,84,b)]. given #101 (A,wt=13): 114 - Ex1(A,x,W) | - Enc(x,f7(c1,x)) | Property(f8(c1,x)) | c1 = x. [resolve(81,a,68,a),flip(d)]. given #102 (F,wt=4): 228 - Enc(c2,f7(c1,c2)) | Property(f8(c1,c2)). [resolve(114,a,82,a),flip(c),unit_del(c,60)]. given #103 (F,wt=9): 224 Enc(c1,f7(c1,c2)) | - Property(f8(c1,c2)) | Proposition(f2(c2,f8(c1,c2))). [resolve(217,b,84,b)]. given #104 (T,wt=11): 196 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Proposition(f3(c2,f8(c2,c1))) | Property(f4(c2)). [resolve(191,b,153,b)]. given #105 (T,wt=9): 229 Property(f7(c2,c1)) | Proposition(f3(c2,f8(c2,c1))) | Property(f4(c2)). [resolve(196,b,188,b),merge(d)]. given #106 (A,wt=13): 115 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(81,a,67,b)]. given #107 (F,wt=4): 230 Enc(c2,f7(c2,c1)) | Property(f8(c2,c1)). [resolve(115,a,82,a),flip(c),unit_del(c,60)]. given #108 (F,wt=6): 235 Property(f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)). [resolve(230,a,94,b)]. given #109 (T,wt=9): 237 Property(f8(c2,c1)) | - Property(f7(c2,c1)) | Proposition(f2(c2,f7(c2,c1))). [resolve(230,a,84,b)]. given #110 (T,wt=11): 197 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Proposition(f3(c2,f8(c2,c1))) | Enc(c2,f4(c2)). [resolve(191,b,152,b)]. given #111 (A,wt=13): 118 - Ex1(A,x,W) | Property(f7(c1,x)) | Enc(x,f8(c1,x)) | c1 = x. [resolve(81,a,66,a),flip(d)]. given #112 (F,wt=4): 239 Property(f7(c1,c2)) | Enc(c2,f8(c1,c2)). [resolve(118,a,82,a),flip(c),unit_del(c,60)]. given #113 (F,wt=6): 244 Property(f7(c1,c2)) | - Property(f8(c1,c2)) | Enc(c1,f8(c1,c2)). [resolve(239,b,94,b)]. given #114 (T,wt=9): 238 Property(f7(c2,c1)) | Proposition(f3(c2,f8(c2,c1))) | Enc(c2,f4(c2)). [resolve(197,b,188,b),merge(d)]. given #115 (T,wt=9): 246 Property(f7(c1,c2)) | - Property(f8(c1,c2)) | Proposition(f2(c2,f8(c1,c2))). [resolve(239,b,84,b)]. given #116 (A,wt=13): 119 - Ex1(A,x,W) | Property(f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(81,a,65,b)]. given #117 (F,wt=4): 250 Property(f7(c2,c1)) | - Enc(c2,f8(c2,c1)). [resolve(119,a,82,a),flip(c),unit_del(c,60)]. given #118 (F,wt=2): 251 Property(f7(c2,c1)). [resolve(250,b,191,b),merge(b)]. given #119 (T,wt=4): 254 Property(f8(c2,c1)) | Enc(c1,f7(c2,c1)). [back_unit_del(235),unit_del(b,251)]. given #120 (T,wt=2): 266 Property(f8(c2,c1)). [resolve(254,b,168,a),merge(b)]. given #121 (A,wt=12): 123 - Ex1(A,x,W) | Property(f7(c1,x)) | Property(f8(c1,x)) | c1 = x. [resolve(81,a,63,a),flip(d)]. given #122 (F,wt=4): 261 Enc(c1,f8(c2,c1)) | Enc(c1,f7(c2,c1)). [back_unit_del(207),unit_del(b,251)]. given #123 (F,wt=4): 267 Property(f7(c1,c2)) | Property(f8(c1,c2)). [resolve(123,a,82,a),flip(c),unit_del(c,60)]. given #124 (T,wt=4): 272 Enc(c1,f7(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(261,a,93,b),unit_del(b,266)]. given #125 (T,wt=4): 276 Property(f7(c1,c2)) | Enc(c1,f8(c1,c2)). [resolve(267,b,244,b),merge(b)]. given #126 (A,wt=16): 126 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c2,y) | - Enc(c2,f6(x,c2)). [resolve(82,a,78,g),unit_del(c,80)]. given #127 (F,wt=2): 284 Property(f7(c1,c2)). [resolve(276,b,186,b),merge(b)]. given #128 (F,wt=4): 277 Enc(c1,f7(c2,c1)) | Enc(c2,f7(c2,c1)). [resolve(272,b,226,b)]. given #129 (T,wt=2): 296 Enc(c1,f7(c2,c1)). [resolve(277,b,94,b),merge(c),unit_del(b,251)]. given #130 (T,wt=2): 298 Enc(c1,f8(c2,c1)). [back_unit_del(166),unit_del(a,296)]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.00) seconds. % Length of proof is 59. % Level of proof is 14. % Maximum clause weight is 21. % Given clauses 130. 1 Situation(c1). [clausify]. 2 Situation(c2). [clausify]. 3 PartOf(c1,c2). [clausify]. 4 PartOf(c2,c1). [clausify]. 6 - Situation(x) | Object(x). [clausify]. 7 - Object(x) | Ex1(A,x,W) | - Situation(x). [clausify]. 15 - Object(x) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - PartOf(x,y). [clausify]. 39 - Object(c1) | Ex1(A,c1,W). [resolve(7,c,1,a)]. 40 - Object(c2) | Ex1(A,c2,W). [resolve(7,c,2,a)]. 55 - Object(c1) | - Object(c2) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(15,f,3,a)]. 56 - Object(c2) | - Object(c1) | - Property(x) | - Enc(c2,x) | Enc(c1,x). [resolve(15,f,4,a)]. 60 c2 != c1. [clausify]. 63 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. 65 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. 66 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. 67 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. 68 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. 70 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. 71 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. 72 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. 73 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. 79 Object(c1). [resolve(6,a,1,a)]. 80 Object(c2). [resolve(6,a,2,a)]. 81 Ex1(A,c1,W). [copy(39),unit_del(a,79)]. 82 Ex1(A,c2,W). [copy(40),unit_del(a,80)]. 93 - Property(x) | - Enc(c1,x) | Enc(c2,x). [copy(55),unit_del(a,79),unit_del(b,80)]. 94 - Property(x) | - Enc(c2,x) | Enc(c1,x). [copy(56),unit_del(a,80),unit_del(b,79)]. 104 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(81,a,73,b)]. 106 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(81,a,72,b)]. 108 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(81,a,71,b)]. 110 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(81,a,70,b)]. 113 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(81,a,68,b)]. 115 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(81,a,67,b)]. 117 - Ex1(A,x,W) | Property(f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(81,a,66,b)]. 119 - Ex1(A,x,W) | Property(f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(81,a,65,b)]. 122 - Ex1(A,x,W) | Property(f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(81,a,63,b)]. 166 - Enc(c1,f7(c2,c1)) | Enc(c1,f8(c2,c1)). [resolve(104,a,82,a),flip(c),unit_del(c,60)]. 168 - Enc(c1,f7(c2,c1)) | Property(f8(c2,c1)). [resolve(113,a,82,a),flip(c),unit_del(c,60)]. 177 Property(f7(c2,c1)) | Enc(c1,f8(c2,c1)). [resolve(117,a,82,a),flip(c),unit_del(c,60)]. 182 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(177,b,93,b)]. 187 - Enc(c1,f7(c2,c1)) | - Enc(c2,f8(c2,c1)). [resolve(106,a,82,a),flip(c),unit_del(c,60)]. 188 Property(f7(c2,c1)) | Property(f8(c2,c1)). [resolve(122,a,82,a),flip(c),unit_del(c,60)]. 191 Property(f7(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(188,b,182,b),merge(b)]. 202 Enc(c2,f7(c2,c1)) | Enc(c1,f8(c2,c1)). [resolve(108,a,82,a),flip(c),unit_del(c,60)]. 207 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)). [resolve(202,a,94,b)]. 226 Enc(c2,f7(c2,c1)) | - Enc(c2,f8(c2,c1)). [resolve(110,a,82,a),flip(c),unit_del(c,60)]. 230 Enc(c2,f7(c2,c1)) | Property(f8(c2,c1)). [resolve(115,a,82,a),flip(c),unit_del(c,60)]. 235 Property(f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)). [resolve(230,a,94,b)]. 250 Property(f7(c2,c1)) | - Enc(c2,f8(c2,c1)). [resolve(119,a,82,a),flip(c),unit_del(c,60)]. 251 Property(f7(c2,c1)). [resolve(250,b,191,b),merge(b)]. 254 Property(f8(c2,c1)) | Enc(c1,f7(c2,c1)). [back_unit_del(235),unit_del(b,251)]. 261 Enc(c1,f8(c2,c1)) | Enc(c1,f7(c2,c1)). [back_unit_del(207),unit_del(b,251)]. 266 Property(f8(c2,c1)). [resolve(254,b,168,a),merge(b)]. 272 Enc(c1,f7(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(261,a,93,b),unit_del(b,266)]. 277 Enc(c1,f7(c2,c1)) | Enc(c2,f7(c2,c1)). [resolve(272,b,226,b)]. 296 Enc(c1,f7(c2,c1)). [resolve(277,b,94,b),merge(c),unit_del(b,251)]. 297 - Enc(c2,f8(c2,c1)). [back_unit_del(187),unit_del(a,296)]. 298 Enc(c1,f8(c2,c1)). [back_unit_del(166),unit_del(a,296)]. 310 $F. [resolve(298,a,93,b),unit_del(a,266),unit_del(b,297)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=130. Generated=373. Kept=250. proofs=1. Usable=84. Sos=55. Demods=1. Denials=0. Limbo=4, Disabled=162. Hints=0. Megabytes=0.35. User_CPU=0.04, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3772 exit (max_proofs) Wed Jun 14 17:11:55 2006 ============================== continuing FOF reduction multisearch == Starting Subproblem 3 of 3. Child search process 3773 started. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 37 clauses. Predicate elimination: Situation/1. Term ordering decisions: Relation symbol precedence: lex([ Object, Property, Proposition, Enc, PartOf, Ex1, =, Situation ]). Function symbol precedence: lex([ A, W, c1, c2, c3, f2, f3, f5, f6, f7, f8, VAC, f1, f4 ]). After inverse_order: Function symbol precedence: lex([ A, W, c1, c2, c3, f2, f3, f5, f6, f7, f8, VAC, f1, f4 ]). Unfolding symbols: (none). Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (less than 100 clauses) Reasonable options, based on the structure of the clauses: % set(factor), because non-Horn % set(back_unit_deletion), because non-Horn % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=1): 56 PartOf(c1,c2). [clausify]. given #2 (I,wt=1): 57 PartOf(c2,c3). [clausify]. given #3 (I,wt=1): 58 - PartOf(c1,c3). [clausify]. given #4 (I,wt=11): 59 - Object(x) | Ex1(A,x,W) | - Object(y) | - PartOf(x,y). [clausify]. given #5 (I,wt=11): 60 - Object(x) | - Object(y) | Ex1(A,y,W) | - PartOf(x,y). [clausify]. given #6 (I,wt=15): 61 - Object(x) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - PartOf(x,y). [clausify]. given #7 (I,wt=18): 62 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | Property(f4(x)). [clausify]. given #8 (I,wt=19): 63 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. given #9 (I,wt=19): 64 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Property(f5(x,y)). [clausify]. given #10 (I,wt=19): 65 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #11 (I,wt=20): 66 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | Property(f4(x)). [clausify]. given #12 (I,wt=20): 67 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Enc(x,f5(x,y)). [clausify]. given #13 (I,wt=20): 68 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | - Enc(y,f5(x,y)). [clausify]. given #14 (I,wt=20): 69 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #15 (I,wt=20): 70 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #16 (I,wt=20): 71 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #17 (I,wt=20): 72 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Property(f8(x,y)) | y = x. [clausify]. given #18 (I,wt=21): 73 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | Enc(x,f4(x)). [clausify]. given #19 (I,wt=21): 74 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #20 (I,wt=21): 75 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #21 (I,wt=21): 76 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | - Enc(x,f8(x,y)) | y = x. [clausify]. given #22 (I,wt=21): 77 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f7(x,y)) | Enc(y,f8(x,y)) | y = x. [clausify]. given #23 (I,wt=22): 78 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f3(x,y)) | - Ex1(A,x,W) | - Proposition(z) | f4(x) != VAC(z). [copy(33),flip(g)]. given #24 (I,wt=24): 79 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f3(x,y)) = y | - Ex1(A,x,W) | - Proposition(z) | f4(x) != VAC(z). [copy(34),flip(g)]. given #25 (I,wt=24): 80 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | Property(f6(x,y)). [clausify]. given #26 (I,wt=25): 81 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | Enc(x,f6(x,y)). [clausify]. given #27 (I,wt=25): 82 - Object(x) | - Ex1(A,x,W) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - Ex1(A,y,W) | - Enc(y,f6(x,y)). [clausify]. given #28 (I,wt=1): 83 Object(c1). [resolve(7,a,1,a)]. given #29 (I,wt=1): 84 Object(c2). [resolve(7,a,2,a)]. given #30 (I,wt=1): 85 Object(c3). [resolve(7,a,3,a)]. given #31 (I,wt=3): 86 Ex1(A,c1,W). [copy(41),unit_del(a,83)]. given #32 (I,wt=3): 87 Ex1(A,c2,W). [copy(42),unit_del(a,84)]. given #33 (I,wt=3): 88 Ex1(A,c3,W). [copy(43),unit_del(a,85)]. given #34 (I,wt=7): 89 - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [copy(44),unit_del(a,83)]. given #35 (I,wt=7): 90 - Property(x) | - Enc(c2,x) | Proposition(f2(c2,x)). [copy(45),unit_del(a,84)]. given #36 (I,wt=7): 91 - Property(x) | - Enc(c3,x) | Proposition(f2(c3,x)). [copy(46),unit_del(a,85)]. given #37 (I,wt=18): 92 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)) | - Ex1(A,x,W) | Property(f1(x)). [copy(47),merge(e)]. given #38 (I,wt=19): 93 - Object(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)) | - Ex1(A,x,W) | Enc(x,f1(x)). [copy(48),merge(e)]. given #39 (I,wt=22): 94 - Object(x) | - Ex1(A,x,W) | - Proposition(y) | f1(x) != VAC(y) | - Property(z) | - Enc(x,z) | Proposition(f2(x,z)). [copy(49),flip(d),merge(e)]. given #40 (I,wt=9): 95 - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [copy(50),unit_del(a,83)]. given #41 (I,wt=9): 96 - Property(x) | - Enc(c2,x) | VAC(f2(c2,x)) = x. [copy(51),unit_del(a,84)]. given #42 (I,wt=9): 97 - Property(x) | - Enc(c3,x) | VAC(f2(c3,x)) = x. [copy(52),unit_del(a,85)]. given #43 (I,wt=20): 98 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | Property(f1(x)). [copy(53),merge(e)]. given #44 (I,wt=21): 99 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | Enc(x,f1(x)). [copy(54),merge(e)]. given #45 (I,wt=24): 100 - Object(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y | - Ex1(A,x,W) | - Proposition(z) | f1(x) != VAC(z). [copy(55),flip(h),merge(e)]. given #46 (I,wt=9): 101 - Object(x) | Ex1(A,x,W) | - PartOf(x,x). [factor(59,a,c)]. given #47 (I,wt=13): 102 - Object(x) | - Ex1(A,x,W) | PartOf(x,x) | Property(f5(x,x)). [factor(64,a,c),merge(d)]. given #48 (I,wt=14): 103 - Object(x) | - Ex1(A,x,W) | PartOf(x,x) | Enc(x,f5(x,x)). [factor(67,a,c),merge(d)]. given #49 (I,wt=14): 104 - Object(x) | - Ex1(A,x,W) | PartOf(x,x) | - Enc(x,f5(x,x)). [factor(68,a,c),merge(d)]. given #50 (T,wt=3): 210 PartOf(c3,c3) | Property(f5(c3,c3)). [resolve(102,b,88,a),unit_del(a,85)]. % SOS Control: given=50, spent=0/3000 (ticks), new_sos_limit=2147483647, disabled=0, user_seconds=0.02. given #51 (A,wt=6): 105 - Property(x) | - Enc(c2,x) | Enc(c3,x). [resolve(61,f,57,a),unit_del(a,84),unit_del(b,85)]. given #52 (F,wt=2): 209 - Enc(c3,f5(c1,c3)). [ur(68,a,83,a,b,86,a,c,85,a,d,58,a,e,88,a)]. given #53 (F,wt=3): 211 PartOf(c2,c2) | Property(f5(c2,c2)). [resolve(102,b,87,a),unit_del(a,84)]. given #54 (T,wt=3): 212 PartOf(c1,c1) | Property(f5(c1,c1)). [resolve(102,b,86,a),unit_del(a,83)]. given #55 (T,wt=3): 213 PartOf(c3,c3) | Enc(c3,f5(c3,c3)). [resolve(103,b,88,a),unit_del(a,85)]. given #56 (A,wt=6): 106 - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(61,f,56,a),unit_del(a,83),unit_del(b,84)]. given #57 (F,wt=3): 214 PartOf(c2,c2) | Enc(c2,f5(c2,c2)). [resolve(103,b,87,a),unit_del(a,84)]. given #58 (F,wt=3): 215 PartOf(c1,c1) | Enc(c1,f5(c1,c1)). [resolve(103,b,86,a),unit_del(a,83)]. given #59 (T,wt=3): 216 PartOf(c3,c3) | - Enc(c3,f5(c3,c3)). [resolve(104,b,88,a),unit_del(a,85)]. given #60 (T,wt=3): 217 PartOf(c2,c2) | - Enc(c2,f5(c2,c2)). [resolve(104,b,87,a),unit_del(a,84)]. given #61 (A,wt=16): 107 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c1,y) | - Enc(c1,f6(x,c1)). [resolve(86,a,82,g),unit_del(c,83)]. given #62 (F,wt=3): 218 PartOf(c1,c1) | - Enc(c1,f5(c1,c1)). [resolve(104,b,86,a),unit_del(a,83)]. given #63 (F,wt=8): 219 - Property(x) | - Enc(c3,x) | Enc(c1,x) | - Enc(c1,f6(c3,c1)). [resolve(107,b,88,a),unit_del(a,85)]. given #64 (T,wt=8): 220 - Property(x) | - Enc(c2,x) | Enc(c1,x) | - Enc(c1,f6(c2,c1)). [resolve(107,b,87,a),unit_del(a,84)]. given #65 (T,wt=9): 139 - Property(x) | - Enc(c1,x) | Proposition(f3(c1,x)) | Enc(c1,f4(c1)). [resolve(86,a,63,e),unit_del(a,83)]. given #66 (A,wt=17): 108 - Object(x) | - Property(y) | - Enc(c1,y) | Enc(x,y) | - Ex1(A,x,W) | - Enc(x,f6(c1,x)). [resolve(86,a,82,b),unit_del(a,83)]. given #67 (F,wt=8): 221 - Property(x) | - Enc(c1,x) | Enc(c3,x) | - Enc(c3,f6(c1,c3)). [resolve(108,e,88,a),unit_del(a,85)]. given #68 (F,wt=9): 140 - Property(x) | - Enc(c1,x) | Proposition(f3(c1,x)) | Property(f4(c1)). [resolve(86,a,62,e),unit_del(a,83)]. given #69 (T,wt=9): 173 - Property(x) | - Enc(c2,x) | Proposition(f3(c2,x)) | Enc(c2,f4(c2)). [resolve(87,a,63,e),unit_del(a,84)]. given #70 (T,wt=9): 174 - Property(x) | - Enc(c2,x) | Proposition(f3(c2,x)) | Property(f4(c2)). [resolve(87,a,62,e),unit_del(a,84)]. given #71 (A,wt=17): 109 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c1,y) | Enc(x,f6(x,c1)). [resolve(86,a,81,g),unit_del(c,83)]. given #72 (F,wt=8): 222 - Property(x) | - Enc(c3,x) | Enc(c1,x) | Enc(c3,f6(c3,c1)). [resolve(109,b,88,a),unit_del(a,85)]. given #73 (F,wt=8): 223 - Property(x) | - Enc(c2,x) | Enc(c1,x) | Enc(c2,f6(c2,c1)). [resolve(109,b,87,a),unit_del(a,84)]. given #74 (T,wt=9): 207 - Property(x) | - Enc(c3,x) | Proposition(f3(c3,x)) | Enc(c3,f4(c3)). [resolve(88,a,63,e),unit_del(a,85)]. given #75 (T,wt=9): 208 - Property(x) | - Enc(c3,x) | Proposition(f3(c3,x)) | Property(f4(c3)). [resolve(88,a,62,e),unit_del(a,85)]. given #76 (A,wt=16): 110 - Object(x) | - Property(y) | - Enc(c1,y) | Enc(x,y) | - Ex1(A,x,W) | Enc(c1,f6(c1,x)). [resolve(86,a,81,b),unit_del(a,83)]. given #77 (F,wt=8): 224 - Property(x) | - Enc(c1,x) | Enc(c3,x) | Enc(c1,f6(c1,c3)). [resolve(110,e,88,a),unit_del(a,85)]. given #78 (F,wt=11): 121 - Property(x) | - Enc(c1,x) | VAC(f3(c1,x)) = x | Enc(c1,f4(c1)). [resolve(86,a,73,e),unit_del(a,83)]. given #79 (T,wt=11): 130 - Object(x) | - Ex1(A,x,W) | PartOf(x,c1) | - Enc(c1,f5(x,c1)). [resolve(86,a,68,e),unit_del(c,83)]. given #80 (T,wt=3): 225 PartOf(c3,c1) | - Enc(c1,f5(c3,c1)). [resolve(130,b,88,a),unit_del(a,85)]. given #81 (A,wt=16): 111 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Enc(x,y) | Enc(c1,y) | Property(f6(x,c1)). [resolve(86,a,80,g),unit_del(c,83)]. given #82 (F,wt=3): 226 PartOf(c2,c1) | - Enc(c1,f5(c2,c1)). [resolve(130,b,87,a),unit_del(a,84)]. given #83 (F,wt=8): 227 - Property(x) | - Enc(c3,x) | Enc(c1,x) | Property(f6(c3,c1)). [resolve(111,b,88,a),unit_del(a,85)]. given #84 (T,wt=8): 228 - Property(x) | - Enc(c2,x) | Enc(c1,x) | Property(f6(c2,c1)). [resolve(111,b,87,a),unit_del(a,84)]. given #85 (T,wt=11): 133 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Enc(c1,f5(c1,x)). [resolve(86,a,67,b),unit_del(a,83)]. given #86 (A,wt=16): 112 - Object(x) | - Property(y) | - Enc(c1,y) | Enc(x,y) | - Ex1(A,x,W) | Property(f6(c1,x)). [resolve(86,a,80,b),unit_del(a,83)]. given #87 (F,wt=2): 229 Enc(c1,f5(c1,c3)). [resolve(133,c,88,a),unit_del(a,85),unit_del(b,58)]. given #88 (F,wt=4): 232 - Property(f5(c1,c3)) | - Enc(c3,f6(c1,c3)). [resolve(229,a,221,b),unit_del(b,209)]. given #89 (T,wt=4): 231 - Property(f5(c1,c3)) | Enc(c1,f6(c1,c3)). [resolve(229,a,224,b),unit_del(b,209)]. given #90 (T,wt=4): 236 - Property(f5(c1,c3)) | Enc(c2,f5(c1,c3)). [resolve(229,a,106,b)]. given #91 (A,wt=12): 113 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(86,a,77,b)]. given #92 (F,wt=5): 239 - Enc(c1,f7(c3,c1)) | Enc(c1,f8(c3,c1)) | c3 = c1. [resolve(113,a,88,a),flip(c)]. given #93 (F,wt=5): 240 - Enc(c1,f7(c2,c1)) | Enc(c1,f8(c2,c1)) | c2 = c1. [resolve(113,a,87,a),flip(c)]. given #94 (T,wt=7): 238 - Property(f5(c1,c3)) | Proposition(f2(c1,f5(c1,c3))). [resolve(229,a,89,b)]. given #95 (T,wt=8): 230 - Property(x) | - Enc(c1,x) | Enc(c3,x) | Property(f6(c1,c3)). [resolve(112,e,88,a),unit_del(a,85)]. given #96 (A,wt=14): 114 - Ex1(A,x,W) | - Enc(x,f7(c1,x)) | Enc(x,f8(c1,x)) | c1 = x. [resolve(86,a,77,a),flip(d)]. given #97 (F,wt=4): 241 - Property(f5(c1,c3)) | Property(f6(c1,c3)). [resolve(230,b,229,a),unit_del(b,209)]. given #98 (F,wt=5): 242 - Enc(c3,f7(c1,c3)) | Enc(c3,f8(c1,c3)) | c3 = c1. [resolve(114,a,88,a),flip(c)]. given #99 (T,wt=5): 243 - Enc(c2,f7(c1,c2)) | Enc(c2,f8(c1,c2)) | c2 = c1. [resolve(114,a,87,a),flip(c)]. given #100 (T,wt=9): 233 - Property(f5(c1,c3)) | Proposition(f3(c1,f5(c1,c3))) | Property(f4(c1)). [resolve(229,a,140,b)]. given #101 (A,wt=13): 115 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(86,a,76,b)]. given #102 (F,wt=5): 244 - Enc(c1,f7(c3,c1)) | - Enc(c3,f8(c3,c1)) | c3 = c1. [resolve(115,a,88,a),flip(c)]. given #103 (F,wt=5): 245 - Enc(c1,f7(c2,c1)) | - Enc(c2,f8(c2,c1)) | c2 = c1. [resolve(115,a,87,a),flip(c)]. given #104 (T,wt=9): 234 - Property(f5(c1,c3)) | Proposition(f3(c1,f5(c1,c3))) | Enc(c1,f4(c1)). [resolve(229,a,139,b)]. given #105 (T,wt=9): 237 - Property(f5(c1,c3)) | VAC(f2(c1,f5(c1,c3))) = f5(c1,c3). [resolve(229,a,95,b)]. given #106 (A,wt=13): 116 - Ex1(A,x,W) | - Enc(x,f7(c1,x)) | - Enc(c1,f8(c1,x)) | c1 = x. [resolve(86,a,76,a),flip(d)]. given #107 (F,wt=5): 246 - Enc(c3,f7(c1,c3)) | - Enc(c1,f8(c1,c3)) | c3 = c1. [resolve(116,a,88,a),flip(c)]. given #108 (F,wt=5): 247 - Enc(c2,f7(c1,c2)) | - Enc(c1,f8(c1,c2)) | c2 = c1. [resolve(116,a,87,a),flip(c)]. given #109 (T,wt=11): 134 - Property(x) | - Enc(c1,x) | VAC(f3(c1,x)) = x | Property(f4(c1)). [resolve(86,a,66,e),unit_del(a,83)]. given #110 (T,wt=11): 137 - Object(x) | - Ex1(A,x,W) | PartOf(x,c1) | Property(f5(x,c1)). [resolve(86,a,64,e),unit_del(c,83)]. given #111 (A,wt=13): 117 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(86,a,75,b)]. given #112 (F,wt=3): 249 PartOf(c3,c1) | Property(f5(c3,c1)). [resolve(137,b,88,a),unit_del(a,85)]. given #113 (F,wt=3): 250 PartOf(c2,c1) | Property(f5(c2,c1)). [resolve(137,b,87,a),unit_del(a,84)]. given #114 (T,wt=5): 251 Enc(c3,f7(c3,c1)) | Enc(c1,f8(c3,c1)) | c3 = c1. [resolve(117,a,88,a),flip(c)]. given #115 (T,wt=4): 260 Enc(c3,f7(c3,c1)) | Enc(c1,f8(c3,c1)). [para(251(c,1),209(a,1)),unit_del(c,229)]. given #116 (A,wt=13): 118 - Ex1(A,x,W) | Enc(c1,f7(c1,x)) | Enc(x,f8(c1,x)) | c1 = x. [resolve(86,a,75,a),flip(d)]. given #117 (F,wt=5): 252 Enc(c2,f7(c2,c1)) | Enc(c1,f8(c2,c1)) | c2 = c1. [resolve(117,a,87,a),flip(c)]. given #118 (F,wt=4): 271 Enc(c2,f7(c2,c1)) | Enc(c1,f8(c2,c1)). [para(252(c,1),57(a,1)),unit_del(c,58)]. given #119 (T,wt=5): 268 Enc(c1,f7(c1,c3)) | Enc(c3,f8(c1,c3)) | c3 = c1. [resolve(118,a,88,a),flip(c)]. given #120 (T,wt=4): 285 Enc(c1,f7(c1,c3)) | Enc(c3,f8(c1,c3)). [para(268(c,1),209(a,1)),unit_del(c,229)]. given #121 (A,wt=14): 119 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(86,a,74,b)]. given #122 (F,wt=5): 269 Enc(c1,f7(c1,c2)) | Enc(c2,f8(c1,c2)) | c2 = c1. [resolve(118,a,87,a),flip(c)]. given #123 (F,wt=4): 296 Enc(c1,f7(c1,c2)) | Enc(c2,f8(c1,c2)). [para(269(c,1),57(a,1)),unit_del(c,58)]. given #124 (T,wt=5): 293 Enc(c3,f7(c3,c1)) | - Enc(c3,f8(c3,c1)) | c3 = c1. [resolve(119,a,88,a),flip(c)]. given #125 (T,wt=5): 294 Enc(c2,f7(c2,c1)) | - Enc(c2,f8(c2,c1)) | c2 = c1. [resolve(119,a,87,a),flip(c)]. given #126 (A,wt=12): 120 - Ex1(A,x,W) | Enc(c1,f7(c1,x)) | - Enc(c1,f8(c1,x)) | c1 = x. [resolve(86,a,74,a),flip(d)]. given #127 (F,wt=5): 305 Enc(c1,f7(c1,c3)) | - Enc(c1,f8(c1,c3)) | c3 = c1. [resolve(120,a,88,a),flip(c)]. given #128 (F,wt=5): 306 Enc(c1,f7(c1,c2)) | - Enc(c1,f8(c1,c2)) | c2 = c1. [resolve(120,a,87,a),flip(c)]. given #129 (T,wt=6): 277 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c3,f7(c2,c1)). [resolve(271,a,105,b)]. given #130 (T,wt=6): 302 Enc(c1,f7(c1,c2)) | - Property(f8(c1,c2)) | Enc(c3,f8(c1,c2)). [resolve(296,b,105,b)]. given #131 (A,wt=12): 122 - Ex1(A,x,W) | - Enc(c1,f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(86,a,72,b)]. given #132 (F,wt=5): 307 - Enc(c1,f7(c3,c1)) | Property(f8(c3,c1)) | c3 = c1. [resolve(122,a,88,a),flip(c)]. given #133 (F,wt=5): 308 - Enc(c1,f7(c2,c1)) | Property(f8(c2,c1)) | c2 = c1. [resolve(122,a,87,a),flip(c)]. given #134 (T,wt=8): 253 Property(f5(c3,c1)) | - Property(x) | - Enc(c3,x) | Enc(c1,x). [resolve(249,a,61,f),unit_del(b,85),unit_del(c,83)]. given #135 (T,wt=8): 254 Property(f5(c2,c1)) | - Property(x) | - Enc(c2,x) | Enc(c1,x). [resolve(250,a,61,f),unit_del(b,84),unit_del(c,83)]. given #136 (A,wt=13): 123 - Ex1(A,x,W) | - Enc(x,f7(c1,x)) | Property(f8(c1,x)) | c1 = x. [resolve(86,a,72,a),flip(d)]. given #137 (F,wt=5): 313 - Enc(c3,f7(c1,c3)) | Property(f8(c1,c3)) | c3 = c1. [resolve(123,a,88,a),flip(c)]. given #138 (F,wt=5): 314 - Enc(c2,f7(c1,c2)) | Property(f8(c1,c2)) | c2 = c1. [resolve(123,a,87,a),flip(c)]. given #139 (T,wt=8): 261 Enc(c1,f8(c3,c1)) | - Property(f7(c3,c1)) | Enc(c1,f7(c3,c1)) | Property(f6(c3,c1)). [resolve(260,a,227,b)]. given #140 (T,wt=8): 262 Enc(c1,f8(c3,c1)) | - Property(f7(c3,c1)) | Enc(c1,f7(c3,c1)) | Enc(c3,f6(c3,c1)). [resolve(260,a,222,b)]. given #141 (A,wt=13): 124 - Ex1(A,x,W) | Enc(x,f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(86,a,71,b)]. given #142 (F,wt=5): 315 Enc(c3,f7(c3,c1)) | Property(f8(c3,c1)) | c3 = c1. [resolve(124,a,88,a),flip(c)]. given #143 (F,wt=4): 322 Enc(c3,f7(c3,c1)) | Property(f8(c3,c1)). [para(315(c,1),209(a,1)),unit_del(c,229)]. given #144 (T,wt=5): 316 Enc(c2,f7(c2,c1)) | Property(f8(c2,c1)) | c2 = c1. [resolve(124,a,87,a),flip(c)]. given #145 (T,wt=4): 332 Enc(c2,f7(c2,c1)) | Property(f8(c2,c1)). [para(316(c,1),57(a,1)),unit_del(c,58)]. given #146 (A,wt=12): 125 - Ex1(A,x,W) | Enc(c1,f7(c1,x)) | Property(f8(c1,x)) | c1 = x. [resolve(86,a,71,a),flip(d)]. given #147 (F,wt=5): 342 Enc(c1,f7(c1,c3)) | Property(f8(c1,c3)) | c3 = c1. [resolve(125,a,88,a),flip(c)]. given #148 (F,wt=4): 349 Enc(c1,f7(c1,c3)) | Property(f8(c1,c3)). [para(342(c,1),209(a,1)),unit_del(c,229)]. given #149 (T,wt=5): 343 Enc(c1,f7(c1,c2)) | Property(f8(c1,c2)) | c2 = c1. [resolve(125,a,87,a),flip(c)]. given #150 (T,wt=4): 361 Enc(c1,f7(c1,c2)) | Property(f8(c1,c2)). [para(343(c,1),57(a,1)),unit_del(c,58)]. given #151 (A,wt=12): 126 - Ex1(A,x,W) | Property(f7(x,c1)) | Enc(c1,f8(x,c1)) | c1 = x. [resolve(86,a,70,b)]. given #152 (F,wt=5): 372 Property(f7(c3,c1)) | Enc(c1,f8(c3,c1)) | c3 = c1. [resolve(126,a,88,a),flip(c)]. given #153 (F,wt=4): 379 Property(f7(c3,c1)) | Enc(c1,f8(c3,c1)). [para(372(c,1),209(a,1)),unit_del(c,229)]. given #154 (T,wt=5): 373 Property(f7(c2,c1)) | Enc(c1,f8(c2,c1)) | c2 = c1. [resolve(126,a,87,a),flip(c)]. given #155 (T,wt=4): 391 Property(f7(c2,c1)) | Enc(c1,f8(c2,c1)). [para(373(c,1),57(a,1)),unit_del(c,58)]. given #156 (A,wt=13): 127 - Ex1(A,x,W) | Property(f7(c1,x)) | Enc(x,f8(c1,x)) | c1 = x. [resolve(86,a,70,a),flip(d)]. given #157 (F,wt=5): 402 Property(f7(c1,c3)) | Enc(c3,f8(c1,c3)) | c3 = c1. [resolve(127,a,88,a),flip(c)]. given #158 (F,wt=4): 409 Property(f7(c1,c3)) | Enc(c3,f8(c1,c3)). [para(402(c,1),209(a,1)),unit_del(c,229)]. given #159 (T,wt=5): 403 Property(f7(c1,c2)) | Enc(c2,f8(c1,c2)) | c2 = c1. [resolve(127,a,87,a),flip(c)]. given #160 (T,wt=4): 419 Property(f7(c1,c2)) | Enc(c2,f8(c1,c2)). [para(403(c,1),57(a,1)),unit_del(c,58)]. given #161 (A,wt=13): 128 - Ex1(A,x,W) | Property(f7(x,c1)) | - Enc(x,f8(x,c1)) | c1 = x. [resolve(86,a,69,b)]. given #162 (F,wt=5): 429 Property(f7(c3,c1)) | - Enc(c3,f8(c3,c1)) | c3 = c1. [resolve(128,a,88,a),flip(c)]. given #163 (F,wt=5): 430 Property(f7(c2,c1)) | - Enc(c2,f8(c2,c1)) | c2 = c1. [resolve(128,a,87,a),flip(c)]. given #164 (T,wt=6): 339 Property(f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c3,f7(c2,c1)). [resolve(332,a,105,b)]. given #165 (T,wt=6): 357 Property(f8(c1,c3)) | - Property(f7(c1,c3)) | Enc(c2,f7(c1,c3)). [resolve(349,a,106,b)]. given #166 (A,wt=12): 129 - Ex1(A,x,W) | Property(f7(c1,x)) | - Enc(c1,f8(c1,x)) | c1 = x. [resolve(86,a,69,a),flip(d)]. given #167 (F,wt=5): 431 Property(f7(c1,c3)) | - Enc(c1,f8(c1,c3)) | c3 = c1. [resolve(129,a,88,a),flip(c)]. given #168 (F,wt=5): 432 Property(f7(c1,c2)) | - Enc(c1,f8(c1,c2)) | c2 = c1. [resolve(129,a,87,a),flip(c)]. given #169 (T,wt=6): 369 Property(f8(c1,c2)) | - Property(f7(c1,c2)) | Enc(c2,f7(c1,c2)). [resolve(361,a,106,b)]. given #170 (T,wt=6): 387 Property(f7(c3,c1)) | - Property(f8(c3,c1)) | Enc(c2,f8(c3,c1)). [resolve(379,b,106,b)]. given #171 (A,wt=12): 131 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | - Enc(x,f5(c1,x)). [resolve(86,a,68,b),unit_del(a,83)]. given #172 (F,wt=6): 399 Property(f7(c2,c1)) | - Property(f8(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(391,b,106,b)]. given #173 (F,wt=6): 426 Property(f7(c1,c2)) | - Property(f8(c1,c2)) | Enc(c3,f8(c1,c2)). [resolve(419,b,105,b)]. given #174 (T,wt=8): 263 Enc(c1,f8(c3,c1)) | - Property(f7(c3,c1)) | Enc(c1,f7(c3,c1)) | - Enc(c1,f6(c3,c1)). [resolve(260,a,219,b)]. given #175 (T,wt=8): 272 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)) | Property(f6(c2,c1)). [resolve(271,a,228,b)]. given #176 (A,wt=12): 132 - Object(x) | - Ex1(A,x,W) | PartOf(x,c1) | Enc(x,f5(x,c1)). [resolve(86,a,67,e),unit_del(c,83)]. given #177 (F,wt=3): 433 PartOf(c3,c1) | Enc(c3,f5(c3,c1)). [resolve(132,b,88,a),unit_del(a,85)]. given #178 (F,wt=3): 434 PartOf(c2,c1) | Enc(c2,f5(c2,c1)). [resolve(132,b,87,a),unit_del(a,84)]. given #179 (T,wt=8): 273 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)) | Enc(c2,f6(c2,c1)). [resolve(271,a,223,b)]. given #180 (T,wt=8): 274 Enc(c1,f8(c2,c1)) | - Property(f7(c2,c1)) | Enc(c1,f7(c2,c1)) | - Enc(c1,f6(c2,c1)). [resolve(271,a,220,b)]. given #181 (A,wt=12): 135 - Ex1(A,x,W) | Property(f7(x,c1)) | Property(f8(x,c1)) | c1 = x. [resolve(86,a,65,b)]. given #182 (F,wt=5): 437 Property(f7(c3,c1)) | Property(f8(c3,c1)) | c3 = c1. [resolve(135,a,88,a),flip(c)]. given #183 (F,wt=4): 444 Property(f7(c3,c1)) | Property(f8(c3,c1)). [para(437(c,1),209(a,1)),unit_del(c,229)]. given #184 (T,wt=4): 445 Property(f7(c3,c1)) | Enc(c2,f8(c3,c1)). [resolve(444,b,387,b),merge(b)]. given #185 (T,wt=5): 438 Property(f7(c2,c1)) | Property(f8(c2,c1)) | c2 = c1. [resolve(135,a,87,a),flip(c)]. given #186 (A,wt=12): 136 - Ex1(A,x,W) | Property(f7(c1,x)) | Property(f8(c1,x)) | c1 = x. [resolve(86,a,65,a),flip(d)]. given #187 (F,wt=4): 452 Property(f7(c2,c1)) | Property(f8(c2,c1)). [para(438(c,1),57(a,1)),unit_del(c,58)]. given #188 (F,wt=4): 455 Property(f7(c2,c1)) | Enc(c2,f8(c2,c1)). [resolve(452,b,399,b),merge(b)]. given #189 (T,wt=3): 456 Property(f7(c2,c1)) | c2 = c1. [resolve(455,b,430,b),merge(b)]. given #190 (T,wt=2): 463 Property(f7(c2,c1)). [para(456(b,1),57(a,1)),unit_del(b,58)]. given #191 (A,wt=11): 138 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Property(f5(c1,x)). [resolve(86,a,64,b),unit_del(a,83)]. given #192 (F,wt=2): 491 - Enc(c3,f6(c1,c3)). [back_unit_del(232),unit_del(a,482)]. given #193 (F,wt=2): 482 Property(f5(c1,c3)). [resolve(138,c,88,a),unit_del(a,85),unit_del(b,58)]. ============================== PROOF ================================= % Proof 1 at 0.07 (+ 0.01) seconds. % Length of proof is 29. % Level of proof is 7. % Maximum clause weight is 20. % Given clauses 193. 1 Situation(c1). [clausify]. 2 Situation(c2). [clausify]. 3 Situation(c3). [clausify]. 7 - Situation(x) | Object(x). [clausify]. 8 - Object(x) | Ex1(A,x,W) | - Situation(x). [clausify]. 41 - Object(c1) | Ex1(A,c1,W). [resolve(8,c,1,a)]. 43 - Object(c3) | Ex1(A,c3,W). [resolve(8,c,3,a)]. 56 PartOf(c1,c2). [clausify]. 57 PartOf(c2,c3). [clausify]. 58 - PartOf(c1,c3). [clausify]. 61 - Object(x) | - Object(y) | - Property(z) | - Enc(x,z) | Enc(y,z) | - PartOf(x,y). [clausify]. 64 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Property(f5(x,y)). [clausify]. 67 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | Enc(x,f5(x,y)). [clausify]. 68 - Object(x) | - Ex1(A,x,W) | - Object(y) | PartOf(x,y) | - Ex1(A,y,W) | - Enc(y,f5(x,y)). [clausify]. 83 Object(c1). [resolve(7,a,1,a)]. 84 Object(c2). [resolve(7,a,2,a)]. 85 Object(c3). [resolve(7,a,3,a)]. 86 Ex1(A,c1,W). [copy(41),unit_del(a,83)]. 88 Ex1(A,c3,W). [copy(43),unit_del(a,85)]. 105 - Property(x) | - Enc(c2,x) | Enc(c3,x). [resolve(61,f,57,a),unit_del(a,84),unit_del(b,85)]. 106 - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(61,f,56,a),unit_del(a,83),unit_del(b,84)]. 133 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Enc(c1,f5(c1,x)). [resolve(86,a,67,b),unit_del(a,83)]. 138 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Property(f5(c1,x)). [resolve(86,a,64,b),unit_del(a,83)]. 209 - Enc(c3,f5(c1,c3)). [ur(68,a,83,a,b,86,a,c,85,a,d,58,a,e,88,a)]. 229 Enc(c1,f5(c1,c3)). [resolve(133,c,88,a),unit_del(a,85),unit_del(b,58)]. 236 - Property(f5(c1,c3)) | Enc(c2,f5(c1,c3)). [resolve(229,a,106,b)]. 482 Property(f5(c1,c3)). [resolve(138,c,88,a),unit_del(a,85),unit_del(b,58)]. 487 Enc(c2,f5(c1,c3)). [back_unit_del(236),unit_del(a,482)]. 493 $F. [ur(105,a,482,a,c,209,a),unit_del(a,487)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=193. Generated=1306. Kept=437. proofs=1. Usable=156. Sos=163. Demods=1. Denials=0. Limbo=0, Disabled=173. Hints=0. Megabytes=0.56. User_CPU=0.07, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3773 exit (max_proofs) Wed Jun 14 17:11:56 2006 ============================== end of multisearch ==================== All 3 subproblems have been proved, so we are done. Total user_CPU=0.12, system_CPU=0.02, wall_clock=1. THEOREM PROVED Exiting. Process 3770 exit (max_proofs) Wed Jun 14 17:11:56 2006