============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 30339 was started by zalta on mally, Fri Sep 11 17:00:17 2009 The command was "prover9.orig". ============================== 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 (9 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 35 clauses. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. ============================== PROOF ================================= % Proof 1 at 1.26 (+ 0.05) seconds. % Length of proof is 520. % Level of proof is 381. % Maximum clause weight is 60. % Given clauses 1577. 5 - Point(x) | Object(f7(x)). [clausify]. 13 - Object(x) | - Point(y) | ActualAt(x,y) | - SituationAt(x,y) | Proposition(f3(x,y)). [clausify]. 14 - Object(x) | - Proposition(y) | - Point(z) | - TrueInAt(y,x,z) | EncpAt(x,y,z). [clausify]. 15 - Object(x) | - Proposition(y) | - Point(z) | TrueInAt(y,x,z) | - EncpAt(x,y,z). [clausify]. 17 - Object(x) | - Point(y) | SituationAt(x,y) | - Ex1At(A,x,y) | Property(f2(x,y)). [clausify]. 18 - Object(x) | - Point(y) | ActualAt(x,y) | - SituationAt(x,y) | - True(f3(x,y),y). [clausify]. 21 - Object(x) | - Point(y) | - ActualAt(x,y) | - Proposition(z) | - TrueInAt(z,x,y) | True(z,y). [clausify]. 22 - Object(x) | - Point(y) | ActualAt(x,y) | - SituationAt(x,y) | TrueInAt(f3(x,y),x,y). [clausify]. 23 - Object(x) | - Point(y) | SituationAt(x,y) | - Ex1At(A,x,y) | EncAt(x,f2(x,y),y). [clausify]. 24 - Object(x) | - Point(y) | WorldAt(x,y) | - SituationAt(x,y) | - Point(z) | Proposition(f5(x,y,z)). [clausify]. 25 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | VAC(y) = f6(x,y,z). [clausify]. 26 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | EncAt(x,f6(x,y,z),z). [clausify]. 29 - Object(x) | - Point(y) | SituationAt(x,y) | - Ex1At(A,x,y) | - Proposition(z) | VAC(z) != f2(x,y). [clausify]. 33 - Object(x) | - Proposition(y) | - Point(z) | EncpAt(x,y,z) | - Property(u) | VAC(y) != u | - EncAt(x,u,z). [clausify]. 34 - Object(x) | - Point(y) | WorldAt(x,y) | - SituationAt(x,y) | - Point(z) | TrueInAt(f5(x,y,z),x,z) | True(f5(x,y,z),z). [clausify]. 35 - Object(x) | - Point(y) | WorldAt(x,y) | - SituationAt(x,y) | - Point(z) | - TrueInAt(f5(x,y,z),x,z) | - True(f5(x,y,z),z). [clausify]. 50 - Proposition(x) | - Point(y) | - EncpAt(f7(z),x,y) | VAC(x) = f6(f7(z),x,y) | - Point(z). [resolve(25,a,5,b)]. 53 - Point(x) | SituationAt(f7(y),x) | - Ex1At(A,f7(y),x) | - Proposition(z) | VAC(z) != f2(f7(y),x) | - Point(y). [resolve(29,a,5,b)]. 60 Point(c1). [clausify]. 61 - WorldAt(x,c1) | - ActualAt(x,c1). [clausify]. 62 - Proposition(x) | Property(VAC(x)). [clausify]. 64 - Point(x) | Ex1At(A,f7(x),x). [clausify]. 65 - Proposition(x) | - Proposition(y) | VAC(y) != VAC(x) | y = x. [clausify]. 66 - Point(x) | - Property(y) | - EncAt(f7(x),y,x) | Proposition(f8(x,y)). [clausify]. 67 - Point(x) | - Property(y) | - EncAt(f7(x),y,x) | True(f8(x,y),x). [clausify]. 68 - Point(x) | - Property(y) | - EncAt(f7(x),y,x) | VAC(f8(x,y)) = y. [clausify]. 69 - Point(x) | - Property(y) | EncAt(f7(x),y,x) | - Proposition(z) | - True(z,x) | VAC(z) != y. [clausify]. 74 - Point(x) | ActualAt(f7(y),x) | - SituationAt(f7(y),x) | Proposition(f3(f7(y),x)) | - Point(y). [resolve(13,a,5,b)]. 75 - Proposition(x) | - Point(y) | - TrueInAt(x,f7(z),y) | EncpAt(f7(z),x,y) | - Point(z). [resolve(14,a,5,b)]. 76 - Proposition(x) | - Point(y) | TrueInAt(x,f7(z),y) | - EncpAt(f7(z),x,y) | - Point(z). [resolve(15,a,5,b)]. 77 - Point(x) | SituationAt(f7(y),x) | - Ex1At(A,f7(y),x) | Property(f2(f7(y),x)) | - Point(y). [resolve(17,a,5,b)]. 78 - Point(x) | ActualAt(f7(y),x) | - SituationAt(f7(y),x) | - True(f3(f7(y),x),x) | - Point(y). [resolve(18,a,5,b)]. 80 - Point(x) | - ActualAt(f7(y),x) | - Proposition(z) | - TrueInAt(z,f7(y),x) | True(z,x) | - Point(y). [resolve(21,a,5,b)]. 81 - Point(x) | ActualAt(f7(y),x) | - SituationAt(f7(y),x) | TrueInAt(f3(f7(y),x),f7(y),x) | - Point(y). [resolve(22,a,5,b)]. 82 - Point(x) | SituationAt(f7(y),x) | - Ex1At(A,f7(y),x) | EncAt(f7(y),f2(f7(y),x),x) | - Point(y). [resolve(23,a,5,b)]. 83 - Point(x) | WorldAt(f7(y),x) | - SituationAt(f7(y),x) | - Point(z) | Proposition(f5(f7(y),x,z)) | - Point(y). [resolve(24,a,5,b)]. 84 - Proposition(x) | - Point(y) | - EncpAt(f7(z),x,y) | f6(f7(z),x,y) = VAC(x) | - Point(z). [copy(50),flip(d)]. 85 - Proposition(x) | - Point(y) | - EncpAt(f7(z),x,y) | EncAt(f7(z),f6(f7(z),x,y),y) | - Point(z). [resolve(26,a,5,b)]. 87 - Point(x) | SituationAt(f7(y),x) | - Ex1At(A,f7(y),x) | - Proposition(z) | f2(f7(y),x) != VAC(z) | - Point(y). [copy(53),flip(e)]. 91 - Proposition(x) | - Point(y) | EncpAt(f7(z),x,y) | - Property(u) | VAC(x) != u | - EncAt(f7(z),u,y) | - Point(z). [resolve(33,a,5,b)]. 92 - Point(x) | WorldAt(f7(y),x) | - SituationAt(f7(y),x) | - Point(z) | TrueInAt(f5(f7(y),x,z),f7(y),z) | True(f5(f7(y),x,z),z) | - Point(y). [resolve(34,a,5,b)]. 93 - Point(x) | WorldAt(f7(y),x) | - SituationAt(f7(y),x) | - Point(z) | - TrueInAt(f5(f7(y),x,z),f7(y),z) | - True(f5(f7(y),x,z),z) | - Point(y). [resolve(35,a,5,b)]. 97 - Point(x) | ActualAt(f7(x),x) | - SituationAt(f7(x),x) | Proposition(f3(f7(x),x)). [factor(74,a,e)]. 98 - Proposition(x) | - Point(y) | - TrueInAt(x,f7(y),y) | EncpAt(f7(y),x,y). [factor(75,b,e)]. 99 - Proposition(x) | - Point(y) | TrueInAt(x,f7(y),y) | - EncpAt(f7(y),x,y). [factor(76,b,e)]. 100 - Point(x) | SituationAt(f7(x),x) | - Ex1At(A,f7(x),x) | Property(f2(f7(x),x)). [factor(77,a,e)]. 101 - Point(x) | ActualAt(f7(x),x) | - SituationAt(f7(x),x) | - True(f3(f7(x),x),x). [factor(78,a,e)]. 103 - Point(x) | - ActualAt(f7(x),x) | - Proposition(y) | - TrueInAt(y,f7(x),x) | True(y,x). [factor(80,a,f)]. 104 - Point(x) | ActualAt(f7(x),x) | - SituationAt(f7(x),x) | TrueInAt(f3(f7(x),x),f7(x),x). [factor(81,a,e)]. 105 - Point(x) | SituationAt(f7(x),x) | - Ex1At(A,f7(x),x) | EncAt(f7(x),f2(f7(x),x),x). [factor(82,a,e)]. 106 - Point(x) | WorldAt(f7(y),x) | - SituationAt(f7(y),x) | Proposition(f5(f7(y),x,x)) | - Point(y). [factor(83,a,d)]. 109 - Proposition(x) | - Point(y) | - EncpAt(f7(y),x,y) | f6(f7(y),x,y) = VAC(x). [factor(84,b,e)]. 110 - Proposition(x) | - Point(y) | - EncpAt(f7(y),x,y) | EncAt(f7(y),f6(f7(y),x,y),y). [factor(85,b,e)]. 112 - Point(x) | SituationAt(f7(x),x) | - Ex1At(A,f7(x),x) | - Proposition(y) | f2(f7(x),x) != VAC(y). [factor(87,a,f)]. 117 - Point(x) | WorldAt(f7(y),x) | - SituationAt(f7(y),x) | TrueInAt(f5(f7(y),x,x),f7(y),x) | True(f5(f7(y),x,x),x) | - Point(y). [factor(92,a,d)]. 120 - Point(x) | WorldAt(f7(y),x) | - SituationAt(f7(y),x) | - TrueInAt(f5(f7(y),x,x),f7(y),x) | - True(f5(f7(y),x,x),x) | - Point(y). [factor(93,a,d)]. 123 - Point(x) | WorldAt(f7(x),x) | - SituationAt(f7(x),x) | Proposition(f5(f7(x),x,x)). [factor(106,a,e)]. 124 - Point(x) | WorldAt(f7(x),x) | - SituationAt(f7(x),x) | TrueInAt(f5(f7(x),x,x),f7(x),x) | True(f5(f7(x),x,x),x). [factor(117,a,f)]. 125 - Point(x) | WorldAt(f7(x),x) | - SituationAt(f7(x),x) | - TrueInAt(f5(f7(x),x,x),f7(x),x) | - True(f5(f7(x),x,x),x). [factor(120,a,f)]. 126 Ex1At(A,f7(c1),c1). [resolve(64,a,60,a)]. 127 - Point(x) | - Property(VAC(y)) | EncAt(f7(x),VAC(y),x) | - Proposition(y) | - True(y,x). [xx_res(69,f)]. 128 - Proposition(x) | - Point(y) | EncpAt(f7(z),x,y) | - Property(VAC(x)) | - EncAt(f7(z),VAC(x),y) | - Point(z). [xx_res(91,e)]. 129 - Proposition(x) | - Point(y) | EncpAt(f7(y),x,y) | - Property(VAC(x)) | - EncAt(f7(y),VAC(x),y). [factor(128,b,f)]. 130 SituationAt(f7(c1),c1) | EncAt(f7(c1),f2(f7(c1),c1),c1). [resolve(126,a,105,c),unit_del(a,60)]. 131 SituationAt(f7(c1),c1) | Property(f2(f7(c1),c1)). [resolve(126,a,100,c),unit_del(a,60)]. 132 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(131,a,124,c),unit_del(b,60)]. 133 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | Proposition(f5(f7(c1),c1,c1)). [resolve(131,a,123,c),unit_del(b,60)]. 136 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(131,a,104,c),unit_del(b,60)]. 137 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | Proposition(f3(f7(c1),c1)). [resolve(131,a,97,c),unit_del(b,60)]. 138 SituationAt(f7(c1),c1) | - Property(f2(f7(c1),c1)) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1). [resolve(130,b,68,c),unit_del(b,60)]. 140 SituationAt(f7(c1),c1) | - Property(f2(f7(c1),c1)) | Proposition(f8(c1,f2(f7(c1),c1))). [resolve(130,b,66,c),unit_del(b,60)]. 143 Property(f2(f7(c1),c1)) | Proposition(f3(f7(c1),c1)) | - WorldAt(f7(c1),c1). [resolve(137,b,61,b)]. 144 Property(f2(f7(c1),c1)) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(143,c,133,b),merge(c)]. 145 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | - Proposition(f3(f7(c1),c1)) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(136,c,98,c),unit_del(d,60)]. 146 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(132,c,103,d),merge(g),unit_del(d,60)]. 148 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | Proposition(f3(f7(c1),c1)). [resolve(146,d,137,b),merge(e)]. 151 SituationAt(f7(c1),c1) | Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(140,b,144,a)]. 153 SituationAt(f7(c1),c1) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(138,b,144,a)]. 158 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | WorldAt(f7(c1),c1). [resolve(151,a,123,c),merge(f),unit_del(d,60)]. 160 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(151,a,97,c),merge(f),unit_del(d,60)]. 166 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(160,d,61,b)]. 170 SituationAt(f7(c1),c1) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | - Proposition(f8(c1,f2(f7(c1),c1))). [resolve(153,b,112,e(flip)),merge(e),unit_del(d,60),unit_del(e,126)]. 176 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(166,d,158,d),merge(d),merge(e),merge(f)]. 181 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(176,c,148,d),merge(f)]. 182 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(VAC(f5(f7(c1),c1,c1))). [resolve(176,c,62,a)]. 186 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(181,d,143,c),merge(e),merge(f)]. 187 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(186,d,127,e),unit_del(d,60)]. 188 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(187,d,182,c),merge(f),merge(g)]. 189 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(188,e,176,c),merge(e),merge(f)]. 191 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(189,d,129,e),unit_del(e,60)]. 197 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(191,f,182,c),merge(f),merge(g)]. 198 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(197,d,176,c),merge(e),merge(f)]. 202 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(198,d,99,d),unit_del(e,60)]. 204 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(202,d,176,c),merge(e),merge(f)]. 205 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(204,d,125,d),unit_del(d,60)]. 206 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(205,f,186,d),merge(f),merge(g),merge(h)]. 207 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(206,e,131,a),merge(e)]. 209 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)). [resolve(207,d,143,c),merge(d),merge(e)]. 210 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | SituationAt(f7(c1),c1). [resolve(209,c,140,b),merge(d)]. 211 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(210,c,124,c),unit_del(c,60)]. 215 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | ActualAt(f7(c1),c1). [resolve(210,c,97,c),merge(e),unit_del(c,60)]. 216 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | - WorldAt(f7(c1),c1). [resolve(215,c,61,b)]. 222 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(211,d,103,d),merge(h),unit_del(e,60)]. 224 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(222,e,215,c),merge(f),merge(g)]. 229 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(224,e,176,c),merge(e),merge(f)]. 230 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(229,c,216,c),merge(d),merge(e)]. 231 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(230,c,127,e),unit_del(c,60)]. 232 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(231,c,182,c),merge(e),merge(f)]. 235 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(232,d,176,c),merge(d),merge(e)]. 236 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(235,c,129,e),unit_del(d,60)]. 242 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(236,e,182,c),merge(e),merge(f)]. 243 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(242,c,176,c),merge(d),merge(e)]. 247 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(243,c,99,d),unit_del(d,60)]. 248 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(247,c,176,c),merge(d),merge(e)]. 249 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(248,c,125,d),unit_del(c,60)]. 250 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(249,e,230,c),merge(e),merge(f)]. 253 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(250,d,210,c),merge(d),merge(e)]. 254 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f3(f7(c1),c1)). [resolve(253,c,216,c),merge(c),merge(d)]. 256 Proposition(f3(f7(c1),c1)) | SituationAt(f7(c1),c1) | Proposition(f5(f7(c1),c1,c1)). [resolve(254,a,170,d),merge(c)]. 259 Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | WorldAt(f7(c1),c1). [resolve(256,b,123,c),merge(e),unit_del(c,60)]. 261 Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(256,b,97,c),merge(e),unit_del(c,60)]. 266 Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(261,c,61,b)]. 267 Proposition(f3(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(266,c,259,c),merge(c),merge(d)]. 268 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(267,b,148,d),merge(e)]. 269 Proposition(f3(f7(c1),c1)) | Property(VAC(f5(f7(c1),c1,c1))). [resolve(267,b,62,a)]. 271 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(268,c,143,c),merge(d),merge(e)]. 272 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(271,c,127,e),unit_del(c,60)]. 274 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(272,c,269,b),merge(e)]. 275 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(274,d,267,b),merge(d)]. 276 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(275,c,129,e),unit_del(d,60)]. 282 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(276,e,269,b),merge(e)]. 284 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(282,c,267,b),merge(d)]. 288 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(284,c,99,d),unit_del(d,60)]. 289 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(288,c,267,b),merge(d)]. 290 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(289,c,125,d),unit_del(c,60)]. 293 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(290,e,271,c),merge(e),merge(f)]. 294 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(293,d,131,a),merge(d)]. 295 Proposition(f3(f7(c1),c1)) | Property(f2(f7(c1),c1)). [resolve(294,c,143,c),merge(c),merge(d)]. 297 Proposition(f3(f7(c1),c1)) | SituationAt(f7(c1),c1) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1). [resolve(295,b,138,b)]. 304 Proposition(f3(f7(c1),c1)) | SituationAt(f7(c1),c1) | - Proposition(f8(c1,f2(f7(c1),c1))). [resolve(297,c,112,e(flip)),merge(d),unit_del(c,60),unit_del(d,126)]. 305 Proposition(f3(f7(c1),c1)) | SituationAt(f7(c1),c1). [resolve(304,c,254,a),merge(c)]. 306 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(305,b,124,c),unit_del(b,60)]. 310 Proposition(f3(f7(c1),c1)) | ActualAt(f7(c1),c1). [resolve(305,b,97,c),merge(d),unit_del(b,60)]. 312 Proposition(f3(f7(c1),c1)) | - WorldAt(f7(c1),c1). [resolve(310,b,61,b)]. 313 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(306,c,103,d),merge(g),unit_del(d,60)]. 320 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(313,d,310,b),merge(e)]. 321 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(320,d,267,b),merge(d)]. 322 Proposition(f3(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(321,b,312,b),merge(c)]. 323 Proposition(f3(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(322,b,127,e),unit_del(b,60)]. 325 Proposition(f3(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(323,b,269,b),merge(d)]. 326 Proposition(f3(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(325,c,267,b),merge(c)]. 327 Proposition(f3(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(326,b,129,e),unit_del(c,60)]. 333 Proposition(f3(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(327,d,269,b),merge(d)]. 335 Proposition(f3(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(333,b,267,b),merge(c)]. 339 Proposition(f3(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(335,b,99,d),unit_del(c,60)]. 340 Proposition(f3(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(339,b,267,b),merge(c)]. 341 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(340,b,125,d),unit_del(b,60)]. 343 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(341,d,322,b),merge(d)]. 344 Proposition(f3(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(343,c,305,b),merge(c)]. 345 Proposition(f3(f7(c1),c1)). [resolve(344,b,312,b),merge(b)]. 346 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [back_unit_del(145),unit_del(c,345)]. 347 Property(VAC(f3(f7(c1),c1))). [resolve(345,a,62,a)]. 349 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(346,c,110,c),unit_del(c,345),unit_del(d,60)]. 350 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(346,c,109,c),unit_del(c,345),unit_del(d,60)]. 364 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(350(c,1),349(c,2)),merge(c),merge(d)]. 367 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | VAC(f8(c1,VAC(f3(f7(c1),c1)))) = VAC(f3(f7(c1),c1)). [resolve(364,c,68,c),unit_del(c,60),unit_del(d,347)]. 368 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(364,c,67,c),unit_del(c,60),unit_del(d,347)]. 369 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | Proposition(f8(c1,VAC(f3(f7(c1),c1)))). [resolve(364,c,66,c),unit_del(c,60),unit_del(d,347)]. 371 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(368,b,146,d),merge(c)]. 372 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - WorldAt(f7(c1),c1). [resolve(368,b,61,b)]. 373 Property(f2(f7(c1),c1)) | Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(369,b,146,d),merge(c)]. 374 Property(f2(f7(c1),c1)) | Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | - WorldAt(f7(c1),c1). [resolve(369,b,61,b)]. 375 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | Proposition(f5(f7(c1),c1,c1)). [resolve(372,c,133,b),merge(c)]. 376 Property(f2(f7(c1),c1)) | Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)). [resolve(374,c,133,b),merge(c)]. 378 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1) | Proposition(f8(c1,f2(f7(c1),c1))). [resolve(376,a,140,b)]. 380 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1). [resolve(376,a,138,b)]. 388 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | - Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(367,c,65,c),unit_del(c,345)]. 426 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1). [resolve(378,c,123,c),merge(f),unit_del(d,60)]. 427 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(378,c,104,c),unit_del(d,60)]. 438 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1) | - Proposition(f8(c1,f2(f7(c1),c1))). [resolve(380,d,112,e(flip)),merge(e),unit_del(d,60),unit_del(e,126)]. 440 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(427,e,98,c),unit_del(e,345),unit_del(f,60)]. 441 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(440,e,110,c),unit_del(e,345),unit_del(f,60)]. 442 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(440,e,109,c),unit_del(e,345),unit_del(f,60)]. 723 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(442(e,1),441(e,2)),merge(e),merge(f),merge(g),merge(h)]. 728 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1). [resolve(723,e,66,c),merge(g),unit_del(e,60),unit_del(f,347)]. 729 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))) | - WorldAt(f7(c1),c1). [resolve(728,d,61,b)]. 731 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | Proposition(f8(c1,f2(f7(c1),c1))). [resolve(729,d,426,d),merge(d),merge(e),merge(f)]. 733 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(731,b,373,e),merge(d)]. 734 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(VAC(f5(f7(c1),c1,c1))). [resolve(731,b,62,a)]. 742 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(733,d,374,c),merge(e),merge(f)]. 743 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(742,d,127,e),unit_del(d,60)]. 778 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(743,d,734,c),merge(f),merge(g)]. 780 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(778,e,731,b),merge(e),merge(f)]. 781 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(780,d,129,e),unit_del(e,60)]. 788 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(781,f,734,c),merge(f),merge(g)]. 790 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(788,d,731,b),merge(e),merge(f)]. 794 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(790,d,99,d),unit_del(e,60)]. 796 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(794,d,731,b),merge(e),merge(f)]. 801 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(796,d,125,d),unit_del(d,60)]. 803 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(801,f,742,d),merge(f),merge(g),merge(h)]. 804 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(803,e,131,a),merge(e)]. 808 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)). [resolve(804,d,374,c),merge(d),merge(e)]. 813 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | SituationAt(f7(c1),c1). [resolve(808,c,140,b),merge(d)]. 814 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(813,c,124,c),unit_del(c,60)]. 817 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(813,c,104,c),unit_del(c,60)]. 818 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(817,d,98,c),unit_del(d,345),unit_del(e,60)]. 819 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(818,d,110,c),unit_del(d,345),unit_del(e,60)]. 820 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(818,d,109,c),unit_del(d,345),unit_del(e,60)]. 825 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(814,d,103,d),merge(h),unit_del(e,60)]. 852 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(820(d,1),819(d,2)),merge(d),merge(e),merge(f)]. 861 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1). [resolve(852,d,66,c),merge(f),unit_del(d,60),unit_del(e,347)]. 862 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(861,c,825,e),merge(c),merge(d)]. 863 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | - WorldAt(f7(c1),c1). [resolve(861,c,61,b)]. 865 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(862,e,731,b),merge(e),merge(f)]. 870 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | True(f5(f7(c1),c1,c1),c1). [resolve(865,c,863,c),merge(d),merge(e)]. 871 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(870,c,127,e),unit_del(c,60)]. 873 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(871,c,734,c),merge(e),merge(f)]. 875 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(873,d,731,b),merge(d),merge(e)]. 882 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(875,c,129,e),unit_del(d,60)]. 889 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(882,e,734,c),merge(e),merge(f)]. 891 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(889,c,731,b),merge(d),merge(e)]. 895 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(891,c,99,d),unit_del(d,60)]. 897 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(895,c,731,b),merge(d),merge(e)]. 898 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(897,c,125,d),unit_del(c,60)]. 899 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(898,e,870,c),merge(e),merge(f)]. 900 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1). [resolve(899,d,813,c),merge(d),merge(e)]. 901 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f8(c1,f2(f7(c1),c1))). [resolve(900,c,863,c),merge(c),merge(d)]. 904 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(901,a,388,c)]. 955 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1) | Proposition(f5(f7(c1),c1,c1)). [para(904(d,1),375(b,1)),merge(d)]. 972 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(955,c,61,b)]. 975 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | Proposition(f5(f7(c1),c1,c1)). [resolve(972,e,133,b),merge(e),merge(f)]. 989 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(975,c,101,d),unit_del(d,60)]. 990 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(989,e,131,a),merge(e)]. 991 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(990,d,61,b)]. 992 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(991,d,133,b),merge(d),merge(e)]. 997 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1). [resolve(992,b,140,b),merge(d)]. 999 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | WorldAt(f7(c1),c1). [resolve(997,c,123,c),merge(e),unit_del(c,60)]. 1000 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(997,c,104,c),unit_del(c,60)]. 1002 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(1000,d,98,c),unit_del(d,345),unit_del(e,60)]. 1005 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(1002,d,110,c),unit_del(d,345),unit_del(e,60)]. 1006 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(1002,d,109,c),unit_del(d,345),unit_del(e,60)]. 1022 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(1006(d,1),1005(d,2)),merge(d),merge(e),merge(f)]. 1024 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | VAC(f8(c1,VAC(f3(f7(c1),c1)))) = VAC(f3(f7(c1),c1)). [resolve(1022,d,68,c),unit_del(d,60),unit_del(e,347)]. 1025 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(1022,d,67,c),unit_del(d,60),unit_del(e,347)]. 1026 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - WorldAt(f7(c1),c1). [resolve(1025,c,61,b)]. 1027 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(1026,d,999,c),merge(d),merge(e)]. 1032 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | - Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(1024,d,65,c),unit_del(d,345)]. 1493 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(1032,d,901,a),merge(e)]. 1494 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1). [para(1493(d,1),1027(c,1)),merge(d),merge(e)]. 1499 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | True(f3(f7(c1),c1),c1) | - WorldAt(f7(c1),c1). [resolve(1494,c,61,b)]. 1500 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | True(f3(f7(c1),c1),c1). [resolve(1499,d,999,c),merge(d),merge(e)]. 1502 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(1500,c,101,d),unit_del(c,60)]. 1504 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(1502,d,997,c),merge(d),merge(e)]. 1505 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(1504,c,61,b)]. 1506 Proposition(f8(c1,f2(f7(c1),c1))) | Proposition(f5(f7(c1),c1,c1)). [resolve(1505,c,999,c),merge(c),merge(d)]. 1509 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1506,b,371,e)]. 1512 Proposition(f8(c1,f2(f7(c1),c1))) | Property(VAC(f5(f7(c1),c1,c1))). [resolve(1506,b,62,a)]. 1539 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1509,d,372,c),merge(e),merge(f)]. 1540 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1539,d,127,e),unit_del(d,60)]. 1645 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1540,d,1512,b),merge(f)]. 1646 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(1645,e,1506,b),merge(e)]. 1647 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(1646,d,129,e),unit_del(e,60)]. 1653 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1647,f,1512,b),merge(f)]. 1666 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1653,d,1506,b),merge(e)]. 1670 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1666,d,99,d),unit_del(e,60)]. 1671 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1670,d,1506,b),merge(e)]. 1672 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(1671,d,125,d),unit_del(d,60)]. 1692 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(1672,f,1539,d),merge(f),merge(g),merge(h)]. 1693 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1). [resolve(1692,e,131,a),merge(e)]. 1696 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(1693,d,372,c),merge(d),merge(e)]. 1698 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1). [para(904(d,1),1696(c,1)),merge(d),merge(e)]. 1699 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1698,c,146,d),merge(d)]. 1700 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | - WorldAt(f7(c1),c1). [resolve(1698,c,61,b)]. 1704 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1699,f,1506,b),merge(f)]. 1705 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1704,d,1700,d),merge(e),merge(f),merge(g)]. 1706 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1705,d,127,e),unit_del(d,60)]. 1707 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1706,d,1512,b),merge(f)]. 1708 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(1707,e,1506,b),merge(e)]. 1709 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(1708,d,129,e),unit_del(e,60)]. 1723 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1709,f,1512,b),merge(f)]. 1724 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1723,d,1506,b),merge(e)]. 1728 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1724,d,99,d),unit_del(e,60)]. 1729 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1728,d,1506,b),merge(e)]. 1742 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(1729,d,125,d),unit_del(d,60)]. 1743 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(1742,f,1705,d),merge(f),merge(g),merge(h)]. 1744 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1). [resolve(1743,e,131,a),merge(e)]. 1745 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1). [resolve(1744,d,1700,d),merge(d),merge(e),merge(f)]. 1763 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(1745,c,101,d),unit_del(c,60)]. 1764 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1). [resolve(1763,d,131,a),merge(d)]. 1765 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1764,c,146,d),merge(c)]. 1766 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - WorldAt(f7(c1),c1). [resolve(1764,c,61,b)]. 1784 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1765,e,1506,b),merge(e)]. 1786 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(1784,c,1766,c),merge(d),merge(e)]. 1787 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1786,c,127,e),unit_del(c,60)]. 1797 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1787,c,1512,b),merge(e)]. 1798 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(1797,d,1506,b),merge(d)]. 1799 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(1798,c,129,e),unit_del(d,60)]. 1805 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1799,e,1512,b),merge(e)]. 1808 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1805,c,1506,b),merge(d)]. 1812 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1808,c,99,d),unit_del(d,60)]. 1813 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1812,c,1506,b),merge(d)]. 1814 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(1813,c,125,d),unit_del(c,60)]. 1817 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(1814,e,1786,c),merge(e),merge(f)]. 1818 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(1817,d,131,a),merge(d)]. 1819 Proposition(f8(c1,f2(f7(c1),c1))) | Property(f2(f7(c1),c1)). [resolve(1818,c,1766,c),merge(c),merge(d)]. 1820 Proposition(f8(c1,f2(f7(c1),c1))) | SituationAt(f7(c1),c1). [resolve(1819,b,140,b),merge(c)]. 1822 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1820,b,124,c),unit_del(b,60)]. 1825 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(1820,b,104,c),unit_del(b,60)]. 1826 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(1825,c,98,c),unit_del(c,345),unit_del(d,60)]. 1827 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(1826,c,110,c),unit_del(c,345),unit_del(d,60)]. 1828 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(1826,c,109,c),unit_del(c,345),unit_del(d,60)]. 1831 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1822,c,103,d),merge(g),unit_del(d,60)]. 1869 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(1828(c,1),1827(c,2)),merge(c),merge(d)]. 1872 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | VAC(f8(c1,VAC(f3(f7(c1),c1)))) = VAC(f3(f7(c1),c1)). [resolve(1869,c,68,c),unit_del(c,60),unit_del(d,347)]. 1873 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(1869,c,67,c),unit_del(c,60),unit_del(d,347)]. 1874 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1873,b,1831,d),merge(c)]. 1875 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - WorldAt(f7(c1),c1). [resolve(1873,b,61,b)]. 1886 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | - Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(1872,c,65,c),unit_del(c,345)]. 1910 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1874,e,1506,b),merge(e)]. 1912 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(1910,c,1875,c),merge(d),merge(e)]. 1913 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1912,c,127,e),unit_del(c,60)]. 1984 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(1913,c,1512,b),merge(e)]. 1985 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(1984,d,1506,b),merge(d)]. 1988 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(1985,c,129,e),unit_del(d,60)]. 1994 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1988,e,1512,b),merge(e)]. 1995 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(1994,c,1506,b),merge(d)]. 1999 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1995,c,99,d),unit_del(d,60)]. 2000 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(1999,c,1506,b),merge(d)]. 2001 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(2000,c,125,d),unit_del(c,60)]. 2003 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(2001,e,1912,c),merge(e),merge(f)]. 2004 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1). [resolve(2003,d,1820,b),merge(d)]. 2006 Proposition(f8(c1,f2(f7(c1),c1))) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(2004,c,1875,c),merge(c),merge(d)]. 2052 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(1886,c,901,a),merge(d)]. 2054 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1). [para(2052(c,1),2006(b,1)),merge(c)]. 2055 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2054,b,1831,d),merge(c)]. 2056 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | - WorldAt(f7(c1),c1). [resolve(2054,b,61,b)]. 2061 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(2055,e,1506,b),merge(e)]. 2063 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(2061,c,2056,c),merge(d),merge(e)]. 2064 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2063,c,127,e),unit_del(c,60)]. 2065 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2064,c,1512,b),merge(e)]. 2066 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(2065,d,1506,b),merge(d)]. 2076 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(2066,c,129,e),unit_del(d,60)]. 2082 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2076,e,1512,b),merge(e)]. 2083 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2082,c,1506,b),merge(d)]. 2087 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2083,c,99,d),unit_del(d,60)]. 2096 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2087,c,1506,b),merge(d)]. 2097 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(2096,c,125,d),unit_del(c,60)]. 2098 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(2097,e,2063,c),merge(e),merge(f)]. 2099 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1). [resolve(2098,d,1820,b),merge(d)]. 2107 Proposition(f8(c1,f2(f7(c1),c1))) | True(f3(f7(c1),c1),c1). [resolve(2099,c,2056,c),merge(c),merge(d)]. 2109 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(2107,b,101,d),unit_del(b,60)]. 2110 Proposition(f8(c1,f2(f7(c1),c1))) | ActualAt(f7(c1),c1). [resolve(2109,c,1820,b),merge(c)]. 2111 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2110,b,1831,d),merge(b)]. 2112 Proposition(f8(c1,f2(f7(c1),c1))) | - WorldAt(f7(c1),c1). [resolve(2110,b,61,b)]. 2147 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(2111,d,1506,b),merge(d)]. 2148 Proposition(f8(c1,f2(f7(c1),c1))) | True(f5(f7(c1),c1,c1),c1). [resolve(2147,b,2112,b),merge(c)]. 2149 Proposition(f8(c1,f2(f7(c1),c1))) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2148,b,127,e),unit_del(b,60)]. 2169 Proposition(f8(c1,f2(f7(c1),c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2149,b,1512,b),merge(d)]. 2170 Proposition(f8(c1,f2(f7(c1),c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(2169,c,1506,b),merge(c)]. 2171 Proposition(f8(c1,f2(f7(c1),c1))) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(2170,b,129,e),unit_del(c,60)]. 2177 Proposition(f8(c1,f2(f7(c1),c1))) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2171,d,1512,b),merge(d)]. 2198 Proposition(f8(c1,f2(f7(c1),c1))) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2177,b,1506,b),merge(c)]. 2202 Proposition(f8(c1,f2(f7(c1),c1))) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2198,b,99,d),unit_del(c,60)]. 2203 Proposition(f8(c1,f2(f7(c1),c1))) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2202,b,1506,b),merge(c)]. 2204 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(2203,b,125,d),unit_del(b,60)]. 2205 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(2204,d,2148,b),merge(d)]. 2206 Proposition(f8(c1,f2(f7(c1),c1))) | WorldAt(f7(c1),c1). [resolve(2205,c,1820,b),merge(c)]. 2207 Proposition(f8(c1,f2(f7(c1),c1))). [resolve(2206,b,2112,b),merge(b)]. 2210 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1). [back_unit_del(438),unit_del(d,2207)]. 2235 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | WorldAt(f7(c1),c1). [resolve(2210,c,123,c),merge(e),unit_del(c,60)]. 2236 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(2210,c,104,c),unit_del(c,60)]. 2250 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(2236,d,98,c),unit_del(d,345),unit_del(e,60)]. 2251 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(2250,d,110,c),unit_del(d,345),unit_del(e,60)]. 2252 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(2250,d,109,c),unit_del(d,345),unit_del(e,60)]. 2734 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(2252(d,1),2251(d,2)),merge(d),merge(e),merge(f)]. 2739 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(2734,d,66,c),merge(f),unit_del(d,60),unit_del(e,347)]. 2740 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(2739,c,61,b)]. 2742 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Proposition(f5(f7(c1),c1,c1)). [resolve(2740,c,2235,c),merge(c),merge(d)]. 2747 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(2742,b,373,e),merge(c)]. 2748 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(VAC(f5(f7(c1),c1,c1))). [resolve(2742,b,62,a)]. 2760 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(2747,c,374,c),merge(d),merge(e)]. 2761 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2760,c,127,e),unit_del(c,60)]. 2762 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2761,c,2748,b),merge(e)]. 2770 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(2762,d,2742,b),merge(d)]. 2771 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(2770,c,129,e),unit_del(d,60)]. 2777 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2771,e,2748,b),merge(e)]. 2778 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2777,c,2742,b),merge(d)]. 2788 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2778,c,99,d),unit_del(d,60)]. 2789 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2788,c,2742,b),merge(d)]. 2790 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(2789,c,125,d),unit_del(c,60)]. 2791 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(2790,e,2760,c),merge(e),merge(f)]. 2806 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(2791,d,131,a),merge(d)]. 2811 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | Property(f2(f7(c1),c1)). [resolve(2806,c,374,c),merge(c),merge(d)]. 2813 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | SituationAt(f7(c1),c1) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1). [resolve(2811,b,138,b)]. 2839 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | SituationAt(f7(c1),c1). [resolve(2813,c,112,e(flip)),merge(d),unit_del(c,60),unit_del(d,126),unit_del(e,2207)]. 2844 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(2839,b,124,c),unit_del(b,60)]. 2847 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(2839,b,104,c),unit_del(b,60)]. 2848 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(2847,c,98,c),unit_del(c,345),unit_del(d,60)]. 2849 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(2848,c,110,c),unit_del(c,345),unit_del(d,60)]. 2850 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(2848,c,109,c),unit_del(c,345),unit_del(d,60)]. 2860 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2844,c,103,d),merge(g),unit_del(d,60)]. 2886 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(2850(c,1),2849(c,2)),merge(c),merge(d)]. 2891 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | ActualAt(f7(c1),c1). [resolve(2886,c,66,c),merge(e),unit_del(c,60),unit_del(d,347)]. 2892 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2891,b,2860,d),merge(b)]. 2893 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | - WorldAt(f7(c1),c1). [resolve(2891,b,61,b)]. 2900 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(2892,d,2742,b),merge(d)]. 2901 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | True(f5(f7(c1),c1,c1),c1). [resolve(2900,b,2893,b),merge(c)]. 2902 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | - Property(VAC(f5(f7(c1),c1,c1))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2901,b,127,e),unit_del(b,60)]. 2903 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1) | - Proposition(f5(f7(c1),c1,c1)). [resolve(2902,b,2748,b),merge(d)]. 2909 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(2903,c,2742,b),merge(c)]. 2910 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1) | - Property(VAC(f5(f7(c1),c1,c1))). [resolve(2909,b,129,e),unit_del(c,60)]. 2916 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | - Proposition(f5(f7(c1),c1,c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2910,d,2748,b),merge(d)]. 2917 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(2916,b,2742,b),merge(c)]. 2921 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | - Proposition(f5(f7(c1),c1,c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2917,b,99,d),unit_del(c,60)]. 2922 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(2921,b,2742,b),merge(c)]. 2923 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(2922,b,125,d),unit_del(b,60)]. 2924 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(2923,d,2901,b),merge(d)]. 2935 Proposition(f8(c1,VAC(f3(f7(c1),c1)))) | WorldAt(f7(c1),c1). [resolve(2924,c,2839,b),merge(c)]. 2936 Proposition(f8(c1,VAC(f3(f7(c1),c1)))). [resolve(2935,b,2893,b),merge(b)]. 3038 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [back_unit_del(388),unit_del(c,2936)]. 3057 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1) | Proposition(f5(f7(c1),c1,c1)). [para(3038(c,1),375(b,1)),merge(c)]. 3059 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(3057,b,61,b)]. 3064 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | Proposition(f5(f7(c1),c1,c1)). [resolve(3059,d,133,b),merge(d),merge(e)]. 3066 Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(3064,b,101,d),unit_del(c,60)]. 3067 Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(3066,d,131,a),merge(d)]. 3070 Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(3067,c,61,b)]. 3071 Property(f2(f7(c1),c1)) | Proposition(f5(f7(c1),c1,c1)). [resolve(3070,c,133,b),merge(c),merge(d)]. 3073 Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1). [resolve(3071,a,138,b)]. 3090 Proposition(f5(f7(c1),c1,c1)) | SituationAt(f7(c1),c1). [resolve(3073,c,112,e(flip)),merge(d),unit_del(c,60),unit_del(d,126),unit_del(e,2207)]. 3092 Proposition(f5(f7(c1),c1,c1)) | WorldAt(f7(c1),c1). [resolve(3090,b,123,c),merge(d),unit_del(b,60)]. 3093 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(3090,b,104,c),unit_del(b,60)]. 3095 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(3093,c,98,c),unit_del(c,345),unit_del(d,60)]. 3100 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(3095,c,110,c),unit_del(c,345),unit_del(d,60)]. 3101 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(3095,c,109,c),unit_del(c,345),unit_del(d,60)]. 3130 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(3101(c,1),3100(c,2)),merge(c),merge(d)]. 3133 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | VAC(f8(c1,VAC(f3(f7(c1),c1)))) = VAC(f3(f7(c1),c1)). [resolve(3130,c,68,c),unit_del(c,60),unit_del(d,347)]. 3134 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(3130,c,67,c),unit_del(c,60),unit_del(d,347)]. 3135 Proposition(f5(f7(c1),c1,c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - WorldAt(f7(c1),c1). [resolve(3134,b,61,b)]. 3136 Proposition(f5(f7(c1),c1,c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(3135,c,3092,b),merge(c)]. 3162 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(3133,c,65,c),unit_del(c,345),unit_del(d,2936)]. 3175 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1). [para(3162(c,1),3136(b,1)),merge(c)]. 3176 Proposition(f5(f7(c1),c1,c1)) | True(f3(f7(c1),c1),c1) | - WorldAt(f7(c1),c1). [resolve(3175,b,61,b)]. 3178 Proposition(f5(f7(c1),c1,c1)) | True(f3(f7(c1),c1),c1). [resolve(3176,c,3092,b),merge(c)]. 3180 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(3178,b,101,d),unit_del(b,60)]. 3181 Proposition(f5(f7(c1),c1,c1)) | ActualAt(f7(c1),c1). [resolve(3180,c,3090,b),merge(c)]. 3182 Proposition(f5(f7(c1),c1,c1)) | - WorldAt(f7(c1),c1). [resolve(3181,b,61,b)]. 3197 Proposition(f5(f7(c1),c1,c1)). [resolve(3182,b,3092,b),merge(b)]. 3213 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [back_unit_del(371),unit_del(e,3197)]. 3216 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1). [back_unit_del(146),unit_del(e,3197)]. 3217 Property(VAC(f5(f7(c1),c1,c1))). [resolve(3197,a,62,a)]. 3342 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3213,c,372,c),merge(d),merge(e)]. 3346 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(3342,c,127,e),unit_del(c,60),unit_del(d,3217),unit_del(f,3197)]. 3385 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(3346,c,129,e),unit_del(c,3197),unit_del(d,60),unit_del(f,3217)]. 3394 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(3385,c,99,d),unit_del(c,3197),unit_del(d,60)]. 3395 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(3394,c,125,d),unit_del(c,60)]. 3483 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(3395,e,3342,c),merge(e),merge(f)]. 3484 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1). [resolve(3483,d,131,a),merge(d)]. 3489 Property(f2(f7(c1),c1)) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(3484,c,372,c),merge(c),merge(d)]. 3491 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1). [para(3038(c,1),3489(b,1)),merge(c)]. 3492 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3491,b,3216,d),merge(c)]. 3493 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | - WorldAt(f7(c1),c1). [resolve(3491,b,61,b)]. 3495 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3492,c,3493,c),merge(d),merge(e)]. 3496 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(3495,c,127,e),unit_del(c,60),unit_del(d,3217),unit_del(f,3197)]. 3501 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(3496,c,129,e),unit_del(c,3197),unit_del(d,60),unit_del(f,3217)]. 3510 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(3501,c,99,d),unit_del(c,3197),unit_del(d,60)]. 3511 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(3510,c,125,d),unit_del(c,60)]. 3512 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(3511,e,3495,c),merge(e),merge(f)]. 3521 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1). [resolve(3512,d,131,a),merge(d)]. 3522 Property(f2(f7(c1),c1)) | True(f3(f7(c1),c1),c1). [resolve(3521,c,3493,c),merge(c),merge(d)]. 3524 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(3522,b,101,d),unit_del(b,60)]. 3525 Property(f2(f7(c1),c1)) | ActualAt(f7(c1),c1). [resolve(3524,c,131,a),merge(c)]. 3530 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3525,b,3216,d),merge(b)]. 3531 Property(f2(f7(c1),c1)) | - WorldAt(f7(c1),c1). [resolve(3525,b,61,b)]. 3544 Property(f2(f7(c1),c1)) | True(f5(f7(c1),c1,c1),c1). [resolve(3530,b,3531,b),merge(c)]. 3545 Property(f2(f7(c1),c1)) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(3544,b,127,e),unit_del(b,60),unit_del(c,3217),unit_del(e,3197)]. 3546 Property(f2(f7(c1),c1)) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(3545,b,129,e),unit_del(b,3197),unit_del(c,60),unit_del(e,3217)]. 3557 Property(f2(f7(c1),c1)) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(3546,b,99,d),unit_del(b,3197),unit_del(c,60)]. 3558 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(3557,b,125,d),unit_del(b,60)]. 3559 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1) | - SituationAt(f7(c1),c1). [resolve(3558,d,3544,b),merge(d)]. 3560 Property(f2(f7(c1),c1)) | WorldAt(f7(c1),c1). [resolve(3559,c,131,a),merge(c)]. 3563 Property(f2(f7(c1),c1)). [resolve(3560,b,3531,b),merge(b)]. 3565 SituationAt(f7(c1),c1) | VAC(f8(c1,f2(f7(c1),c1))) = f2(f7(c1),c1). [back_unit_del(138),unit_del(b,3563)]. 3584 SituationAt(f7(c1),c1). [resolve(3565,b,112,e(flip)),merge(c),unit_del(b,60),unit_del(c,126),unit_del(d,2207)]. 3599 WorldAt(f7(c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3584,a,124,c),unit_del(a,60)]. 3602 ActualAt(f7(c1),c1) | TrueInAt(f3(f7(c1),c1),f7(c1),c1). [resolve(3584,a,104,c),unit_del(a,60)]. 3603 ActualAt(f7(c1),c1) | EncpAt(f7(c1),f3(f7(c1),c1),c1). [resolve(3602,b,98,c),unit_del(b,345),unit_del(c,60)]. 3604 ActualAt(f7(c1),c1) | EncAt(f7(c1),f6(f7(c1),f3(f7(c1),c1),c1),c1). [resolve(3603,b,110,c),unit_del(b,345),unit_del(c,60)]. 3605 ActualAt(f7(c1),c1) | f6(f7(c1),f3(f7(c1),c1),c1) = VAC(f3(f7(c1),c1)). [resolve(3603,b,109,c),unit_del(b,345),unit_del(c,60)]. 3607 WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1) | - ActualAt(f7(c1),c1). [resolve(3599,b,103,d),merge(f),unit_del(c,60),unit_del(e,3197)]. 3624 ActualAt(f7(c1),c1) | EncAt(f7(c1),VAC(f3(f7(c1),c1)),c1). [para(3605(b,1),3604(b,2)),merge(b)]. 3628 ActualAt(f7(c1),c1) | VAC(f8(c1,VAC(f3(f7(c1),c1)))) = VAC(f3(f7(c1),c1)). [resolve(3624,b,68,c),unit_del(b,60),unit_del(c,347)]. 3629 ActualAt(f7(c1),c1) | True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(3624,b,67,c),unit_del(b,60),unit_del(c,347)]. 3630 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3629,a,3607,c)]. 3631 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | - WorldAt(f7(c1),c1). [resolve(3629,a,61,b)]. 3660 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3630,b,3631,b),merge(c)]. 3661 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(3660,b,127,e),unit_del(b,60),unit_del(c,3217),unit_del(e,3197)]. 3689 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(3661,b,129,e),unit_del(b,3197),unit_del(c,60),unit_del(e,3217)]. 3698 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(3689,b,99,d),unit_del(b,3197),unit_del(c,60)]. 3699 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(3698,b,125,d),unit_del(b,60),unit_del(d,3584)]. 3715 True(f8(c1,VAC(f3(f7(c1),c1))),c1) | WorldAt(f7(c1),c1). [resolve(3699,c,3660,b),merge(c)]. 3718 True(f8(c1,VAC(f3(f7(c1),c1))),c1). [resolve(3715,b,3631,b),merge(b)]. 3809 ActualAt(f7(c1),c1) | f8(c1,VAC(f3(f7(c1),c1))) = f3(f7(c1),c1). [resolve(3628,b,65,c),unit_del(b,345),unit_del(c,2936)]. 3826 ActualAt(f7(c1),c1) | True(f3(f7(c1),c1),c1). [para(3809(b,1),3718(a,1))]. 3828 True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3826,a,3607,c)]. 3829 True(f3(f7(c1),c1),c1) | - WorldAt(f7(c1),c1). [resolve(3826,a,61,b)]. 3832 True(f3(f7(c1),c1),c1) | True(f5(f7(c1),c1,c1),c1). [resolve(3828,b,3829,b),merge(c)]. 3833 True(f3(f7(c1),c1),c1) | EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(3832,b,127,e),unit_del(b,60),unit_del(c,3217),unit_del(e,3197)]. 3834 True(f3(f7(c1),c1),c1) | EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [resolve(3833,b,129,e),unit_del(b,3197),unit_del(c,60),unit_del(e,3217)]. 3843 True(f3(f7(c1),c1),c1) | TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [resolve(3834,b,99,d),unit_del(b,3197),unit_del(c,60)]. 3844 True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1) | - True(f5(f7(c1),c1,c1),c1). [resolve(3843,b,125,d),unit_del(b,60),unit_del(d,3584)]. 3845 True(f3(f7(c1),c1),c1) | WorldAt(f7(c1),c1). [resolve(3844,c,3832,b),merge(c)]. 3846 True(f3(f7(c1),c1),c1). [resolve(3845,b,3829,b),merge(b)]. 3848 ActualAt(f7(c1),c1). [resolve(3846,a,101,d),unit_del(a,60),unit_del(c,3584)]. 3849 WorldAt(f7(c1),c1) | True(f5(f7(c1),c1,c1),c1). [back_unit_del(3607),unit_del(c,3848)]. 3850 - WorldAt(f7(c1),c1). [resolve(3848,a,61,b)]. 3851 True(f5(f7(c1),c1,c1),c1). [back_unit_del(3849),unit_del(a,3850)]. 3856 EncAt(f7(c1),VAC(f5(f7(c1),c1,c1)),c1). [resolve(3851,a,127,e),unit_del(a,60),unit_del(b,3217),unit_del(d,3197)]. 3870 - TrueInAt(f5(f7(c1),c1,c1),f7(c1),c1). [ur(125,a,60,a,b,3850,a,c,3584,a,e,3851,a)]. 3871 - EncpAt(f7(c1),f5(f7(c1),c1,c1),c1). [ur(99,a,3197,a,b,60,a,c,3870,a)]. 3890 $F. [ur(129,a,3197,a,b,60,a,c,3871,a,d,3217,a),unit_del(a,3856)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=1577. Generated=11475. Kept=3830. proofs=1. Usable=93. Sos=20. Demods=4. Denials=0. Limbo=0, Disabled=3776. Hints=0. Megabytes=2.44. User_CPU=1.28, System_CPU=0.05, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 30339 exit (max_proofs) Fri Sep 11 17:00:18 2009