============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 13564 was started by zalta on mally, Sat Jul 21 16:05:40 2007 The command was "prove.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 (13 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 34 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 0.17 (+ 0.01) seconds. % Length of proof is 182. % Level of proof is 86. % Maximum clause weight is 24. % Given clauses 437. 1 Point(W). [clausify]. 2 Proposition(L). [clausify]. 9 - Proposition(x) | Property(VAC(x)). [clausify]. 10 Proposition(x) | - Property(VAC(x)). [clausify]. 14 - Object(x) | Actual(x) | - Situation(x) | Proposition(f4(x)). [clausify]. 19 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 20 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 23 - Object(x) | - Proposition(y) | - Encp(x,y) | Property(f1(x,y)). [clausify]. 25 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 27 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 28 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f1(x,y). [clausify]. 30 - Object(x) | - Proposition(y) | - Point(z) | - Ex1At(VAC(y),x,z) | True(y,z). [clausify]. 31 - Object(x) | - Proposition(y) | - Point(z) | Ex1At(VAC(y),x,z) | - True(y,z). [clausify]. 33 - Object(x) | Situation(x) | - Ex1At(A,x,W) | - Proposition(y) | VAC(y) != f3(x). [clausify]. 34 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 35 - Object(x) | - Proposition(y) | - Ex1At(VAC(y),x,W) | True(y,W). [resolve(30,c,1,a)]. 36 - Object(x) | - Proposition(y) | Ex1At(VAC(y),x,W) | - True(y,W). [resolve(31,c,1,a)]. 55 - Object(x) | - Encp(x,y) | VAC(y) = f1(x,y) | - Property(VAC(y)). [resolve(28,b,10,a)]. 56 - Object(x) | - Encp(x,f4(y)) | VAC(f4(y)) = f1(x,f4(y)) | - Object(y) | Actual(y) | - Situation(y). [resolve(28,b,14,d)]. 64 - Object(x) | Situation(x) | - Ex1At(A,x,W) | VAC(L) != f3(x). [resolve(33,d,2,a)]. 65 - Object(x) | Situation(x) | - Ex1At(A,x,W) | VAC(y) != f3(x) | - Property(VAC(y)). [resolve(33,d,10,a)]. 80 Object(c1). [clausify]. 81 Object(c2). [clausify]. 82 True(T,W). [clausify]. 83 Ex1At(A,c1,W). [clausify]. 84 Ex1At(A,c2,W). [clausify]. 85 - True(L,W). [clausify]. 88 - Situation(x) | - Actual(x) | - Situation(y) | Actual(y). [clausify]. 89 - Property(x) | - Enc(c1,x) | VAC(T) = x. [clausify]. 90 - Property(x) | Enc(c1,x) | VAC(T) != x. [clausify]. 91 - Property(x) | - Enc(c2,x) | VAC(L) = x. [clausify]. 92 - Property(x) | Enc(c2,x) | VAC(L) != x. [clausify]. 93 - Object(x) | Actual(x) | - Situation(x) | TrueIn(f4(x),x). [clausify]. 94 - Object(x) | Actual(x) | - Situation(x) | - True(f4(x),W). [clausify]. 95 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Property(f3(x)). [clausify]. 96 - Object(x) | Situation(x) | - Ex1At(A,x,W) | Enc(x,f3(x)). [clausify]. 98 Property(VAC(L)). [resolve(9,a,2,a)]. 102 - Object(x) | - TrueIn(f4(y),x) | Encp(x,f4(y)) | - Object(y) | Actual(y) | - Situation(y). [resolve(19,b,14,d)]. 104 - Object(x) | TrueIn(y,x) | - Encp(x,y) | - Property(VAC(y)). [resolve(20,b,10,a)]. 106 - Object(x) | - Encp(x,L) | Property(f1(x,L)). [resolve(23,b,2,a)]. 108 - Object(x) | - Encp(x,f4(y)) | Property(f1(x,f4(y))) | - Object(y) | Actual(y) | - Situation(y). [resolve(23,b,14,d)]. 111 - Object(x) | - Encp(x,f4(y)) | Enc(x,f1(x,f4(y))) | - Object(y) | Actual(y) | - Situation(y). [resolve(25,b,14,d)]. 113 - Object(x) | - Actual(x) | - TrueIn(y,x) | True(y,W) | - Property(VAC(y)). [resolve(27,c,10,a)]. 116 - Object(x) | - Encp(x,y) | f1(x,y) = VAC(y) | - Property(VAC(y)). [copy(55),flip(c)]. 117 - Object(x) | - Encp(x,f4(y)) | f1(x,f4(y)) = VAC(f4(y)) | - Object(y) | Actual(y) | - Situation(y). [copy(56),flip(c)]. 125 - Object(x) | Situation(x) | - Ex1At(A,x,W) | f3(x) != VAC(L). [copy(64),flip(d)]. 126 - Object(x) | Situation(x) | - Ex1At(A,x,W) | f3(x) != VAC(y) | - Property(VAC(y)). [copy(65),flip(d)]. 130 - Object(x) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z) | - Property(VAC(y)). [resolve(34,b,10,a)]. 135 - Object(x) | - Ex1At(VAC(f4(y)),x,W) | True(f4(y),W) | - Object(y) | Actual(y) | - Situation(y). [resolve(35,b,14,d)]. 137 - Object(x) | Ex1At(VAC(y),x,W) | - True(y,W) | - Property(VAC(y)). [resolve(36,b,10,a)]. 139 - Object(x) | - TrueIn(f4(x),x) | Encp(x,f4(x)) | Actual(x) | - Situation(x). [factor(102,a,d)]. 140 - Object(x) | - Encp(x,f4(x)) | Property(f1(x,f4(x))) | Actual(x) | - Situation(x). [factor(108,a,d)]. 141 - Object(x) | - Encp(x,f4(x)) | Enc(x,f1(x,f4(x))) | Actual(x) | - Situation(x). [factor(111,a,d)]. 142 - Object(x) | - Encp(x,f4(x)) | VAC(f4(x)) = f1(x,f4(x)) | Actual(x) | - Situation(x). [factor(117,a,d),flip(c)]. 149 - Object(x) | Encp(x,y) | - Property(VAC(y)) | - Enc(x,VAC(y)). [factor(130,c,f),xx(d)]. 154 - Object(x) | - Ex1At(VAC(f4(x)),x,W) | True(f4(x),W) | Actual(x) | - Situation(x). [factor(135,a,d)]. 157 - Property(VAC(T)) | Enc(c1,VAC(T)). [xx_res(90,c)]. 158 Enc(c2,VAC(L)). [xx_res(92,c),unit_del(a,98)]. 159 Situation(c2) | Property(f3(c2)). [resolve(95,c,84,a),unit_del(a,81)]. 160 Situation(c1) | Property(f3(c1)). [resolve(95,c,83,a),unit_del(a,80)]. 161 Situation(c2) | Enc(c2,f3(c2)). [resolve(96,c,84,a),unit_del(a,81)]. 162 Situation(c1) | Enc(c1,f3(c1)). [resolve(96,c,83,a),unit_del(a,80)]. 166 - Object(x) | Ex1At(VAC(T),x,W) | - Property(VAC(T)). [resolve(137,c,82,a)]. 167 Encp(c2,L). [resolve(158,a,149,d),unit_del(a,81),unit_del(c,98)]. 170 VAC(L) = f1(c2,L). [resolve(167,a,116,b),flip(b),unit_del(a,81),unit_del(c,98)]. 173 Property(f1(c2,L)). [resolve(167,a,106,b),unit_del(a,81)]. 174 TrueIn(L,c2). [resolve(167,a,104,c),demod(170(7)),unit_del(a,81),unit_del(c,173)]. 182 - Object(x) | Situation(x) | - Ex1At(A,x,W) | f3(x) != f1(c2,L). [back_demod(125),demod(170(8))]. 185 - Property(x) | - Enc(c2,x) | f1(c2,L) = x. [back_demod(91),demod(170(5))]. 186 - Actual(c2). [resolve(174,a,113,c),demod(170(9)),unit_del(a,81),unit_del(c,85),unit_del(d,173)]. 190 Property(f3(c1)) | Actual(c1) | TrueIn(f4(c1),c1). [resolve(160,a,93,c),unit_del(b,80)]. 191 Situation(c1) | - Property(f3(c1)) | f3(c1) = VAC(T). [resolve(162,b,89,b),flip(c)]. 195 Property(f3(c1)) | Actual(c1) | Encp(c1,f4(c1)) | - Situation(c1). [resolve(190,c,139,b),merge(e),unit_del(c,80)]. 206 Property(f3(c1)) | Actual(c1) | Encp(c1,f4(c1)). [resolve(195,d,160,a),merge(d)]. 207 Property(f3(c1)) | Actual(c1) | VAC(f4(c1)) = f1(c1,f4(c1)) | - Situation(c1). [resolve(206,c,142,b),merge(e),unit_del(c,80)]. 208 Property(f3(c1)) | Actual(c1) | Enc(c1,f1(c1,f4(c1))) | - Situation(c1). [resolve(206,c,141,b),merge(e),unit_del(c,80)]. 209 Property(f3(c1)) | Actual(c1) | Property(f1(c1,f4(c1))) | - Situation(c1). [resolve(206,c,140,b),merge(e),unit_del(c,80)]. 213 - Property(f3(c2)) | f3(c2) = f1(c2,L) | Situation(c2). [resolve(185,b,161,b),flip(b)]. 219 Property(f3(c1)) | Actual(c1) | Enc(c1,f1(c1,f4(c1))). [resolve(208,d,160,a),merge(d)]. 222 Property(f3(c1)) | Actual(c1) | - Property(f1(c1,f4(c1))) | f1(c1,f4(c1)) = VAC(T). [resolve(219,c,89,b),flip(d)]. 223 Property(f3(c1)) | Actual(c1) | Property(f1(c1,f4(c1))). [resolve(209,d,160,a),merge(d)]. 224 Property(f3(c1)) | Property(f1(c1,f4(c1))) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(223,b,88,b)]. 270 Property(f3(c1)) | Actual(c1) | VAC(f4(c1)) = f1(c1,f4(c1)). [resolve(207,d,160,a),merge(d)]. 291 Property(f3(c1)) | Actual(c1) | - Ex1At(f1(c1,f4(c1)),c1,W) | True(f4(c1),W) | - Situation(c1). [para(270(c,1),154(b,1)),merge(f),unit_del(c,80)]. 333 Property(f3(c1)) | Property(f1(c1,f4(c1))) | - Situation(x) | Actual(x). [resolve(224,c,160,a),merge(e)]. 334 Property(f3(c1)) | Property(f1(c1,f4(c1))) | - Situation(c1) | Property(f3(c2)). [resolve(224,d,159,a),unit_del(d,186)]. 335 Property(f3(c1)) | Property(f1(c1,f4(c1))) | Property(f3(c2)). [resolve(334,c,160,a),merge(d)]. 338 Property(f3(c1)) | Actual(c1) | f1(c1,f4(c1)) = VAC(T) | Property(f3(c2)). [resolve(222,c,335,b),merge(d)]. 341 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | VAC(f4(c1)) = VAC(T). [para(338(c,1),270(c,2)),merge(d),merge(e)]. 342 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | Property(VAC(T)). [para(338(c,1),335(b,1)),merge(d),merge(f)]. 346 Property(f3(c1)) | Property(f3(c2)) | Property(VAC(T)) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(342,b,88,b)]. 369 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | - Ex1At(VAC(T),c1,W) | True(f4(c1),W) | - Situation(c1). [para(341(d,1),154(b,1)),merge(g),unit_del(d,80)]. 377 Property(f3(c1)) | Property(f3(c2)) | Property(VAC(T)) | - Situation(c1). [resolve(346,e,159,a),merge(f),unit_del(e,186)]. 380 Property(f3(c1)) | Property(f3(c2)) | Property(VAC(T)). [resolve(377,d,160,a),merge(d)]. 381 Property(f3(c1)) | Property(VAC(T)) | f3(c2) = f1(c2,L) | Situation(c2). [resolve(380,b,213,a)]. 382 Property(f3(c1)) | Property(VAC(T)) | Situation(c2). [resolve(381,c,182,d),merge(e),unit_del(d,81),unit_del(e,84)]. 383 Property(f3(c1)) | Property(VAC(T)) | Property(f1(c1,f4(c1))). [resolve(382,c,333,c),merge(c),unit_del(d,186)]. 399 Property(f3(c1)) | Property(VAC(T)) | Actual(c1) | f1(c1,f4(c1)) = VAC(T). [resolve(383,c,222,c),merge(c)]. 434 Property(f3(c1)) | Property(VAC(T)) | Actual(c1). [para(399(d,1),383(c,1)),merge(d),merge(e),merge(f)]. 435 Property(f3(c1)) | Property(VAC(T)) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(434,c,88,b)]. 437 Property(f3(c1)) | Property(VAC(T)) | - Situation(c1). [resolve(435,d,382,c),merge(e),merge(f),unit_del(d,186)]. 438 Property(f3(c1)) | Property(VAC(T)). [resolve(437,c,160,a),merge(c)]. 439 Property(VAC(T)) | Situation(c1) | f3(c1) = VAC(T). [resolve(438,a,191,b)]. 445 Property(VAC(T)) | Situation(c1). [para(439(c,1),438(a,1)),merge(c),merge(d)]. 447 Property(VAC(T)) | Actual(c1) | TrueIn(f4(c1),c1). [resolve(445,b,93,c),unit_del(b,80)]. 449 Property(VAC(T)) | Actual(c1) | Encp(c1,f4(c1)) | - Situation(c1). [resolve(447,c,139,b),merge(e),unit_del(c,80)]. 452 Property(VAC(T)) | Actual(c1) | Encp(c1,f4(c1)). [resolve(449,d,445,b),merge(d)]. 454 Property(VAC(T)) | Actual(c1) | Enc(c1,f1(c1,f4(c1))) | - Situation(c1). [resolve(452,c,141,b),merge(e),unit_del(c,80)]. 455 Property(VAC(T)) | Actual(c1) | Property(f1(c1,f4(c1))) | - Situation(c1). [resolve(452,c,140,b),merge(e),unit_del(c,80)]. 460 Property(VAC(T)) | Actual(c1) | Enc(c1,f1(c1,f4(c1))). [resolve(454,d,445,b),merge(d)]. 463 Property(VAC(T)) | Actual(c1) | - Property(f1(c1,f4(c1))) | f1(c1,f4(c1)) = VAC(T). [resolve(460,c,89,b),flip(d)]. 464 Property(VAC(T)) | Actual(c1) | Property(f1(c1,f4(c1))). [resolve(455,d,445,b),merge(d)]. 465 Property(VAC(T)) | Property(f1(c1,f4(c1))) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(464,b,88,b)]. 493 Property(VAC(T)) | Property(f1(c1,f4(c1))) | - Situation(x) | Actual(x). [resolve(465,c,445,b),merge(e)]. 494 Property(VAC(T)) | Property(f1(c1,f4(c1))) | - Situation(c1) | Property(f3(c2)). [resolve(465,d,159,a),unit_del(d,186)]. 495 Property(VAC(T)) | Property(f1(c1,f4(c1))) | Property(f3(c2)). [resolve(494,c,445,b),merge(d)]. 519 Property(VAC(T)) | Actual(c1) | f1(c1,f4(c1)) = VAC(T) | Property(f3(c2)). [resolve(463,c,495,b),merge(d)]. 522 Property(VAC(T)) | Actual(c1) | Property(f3(c2)). [para(519(c,1),495(b,1)),merge(d),merge(e),merge(f)]. 523 Property(VAC(T)) | Property(f3(c2)) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(522,b,88,b)]. 525 Property(VAC(T)) | Property(f3(c2)) | - Situation(c1). [resolve(523,d,159,a),merge(e),unit_del(d,186)]. 526 Property(VAC(T)) | Property(f3(c2)). [resolve(525,c,445,b),merge(c)]. 527 Property(VAC(T)) | f3(c2) = f1(c2,L) | Situation(c2). [resolve(526,b,213,a)]. 528 Property(VAC(T)) | Situation(c2). [resolve(527,b,182,d),merge(d),unit_del(c,81),unit_del(d,84)]. 529 Property(VAC(T)) | Property(f1(c1,f4(c1))). [resolve(528,b,493,c),merge(b),unit_del(c,186)]. 545 Property(VAC(T)) | Actual(c1) | f1(c1,f4(c1)) = VAC(T). [resolve(529,b,463,c),merge(b)]. 578 Property(VAC(T)) | Actual(c1). [para(545(c,1),529(b,1)),merge(c),merge(d)]. 579 Property(VAC(T)) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(578,b,88,b)]. 581 Property(VAC(T)) | - Situation(c1). [resolve(579,c,528,b),merge(d),unit_del(c,186)]. 582 Property(VAC(T)). [resolve(581,b,445,b),merge(b)]. 603 - Object(x) | Ex1At(VAC(T),x,W). [back_unit_del(166),unit_del(c,582)]. 604 Enc(c1,VAC(T)). [back_unit_del(157),unit_del(a,582)]. 608 Encp(c1,T). [resolve(604,a,149,d),unit_del(a,80),unit_del(c,582)]. 611 VAC(T) = f1(c1,T). [resolve(608,a,116,b),flip(b),unit_del(a,80),unit_del(c,582)]. 617 - Object(x) | Ex1At(f1(c1,T),x,W). [back_demod(603),demod(611(3))]. 622 Property(f1(c1,T)). [back_demod(582),demod(611(2))]. 624 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | - Ex1At(f1(c1,T),c1,W) | True(f4(c1),W) | - Situation(c1). [back_demod(369),demod(611(10))]. 634 Property(f3(c1)) | Actual(c1) | - Property(f1(c1,f4(c1))) | f1(c1,f4(c1)) = f1(c1,T). [back_demod(222),demod(611(16))]. 635 Situation(c1) | - Property(f3(c1)) | f3(c1) = f1(c1,T). [back_demod(191),demod(611(9))]. 637 - Property(x) | - Enc(c1,x) | f1(c1,T) = x. [back_demod(89),demod(611(5))]. 645 - Object(x) | Situation(x) | - Ex1At(A,x,W) | f3(x) != f1(c1,T). [para(611(a,1),126(d,2)),demod(611(12)),unit_del(e,622)]. 648 Ex1At(f1(c1,T),c1,W). [resolve(617,a,80,a)]. 649 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | True(f4(c1),W) | - Situation(c1). [back_unit_del(624),unit_del(d,648)]. 651 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | True(f4(c1),W). [resolve(649,e,160,a),merge(e)]. 653 Property(f3(c1)) | Actual(c1) | Property(f3(c2)) | - Situation(c1). [resolve(651,d,94,d),merge(e),unit_del(d,80)]. 654 Property(f3(c1)) | Actual(c1) | Property(f3(c2)). [resolve(653,d,160,a),merge(d)]. 655 Property(f3(c1)) | Property(f3(c2)) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(654,b,88,b)]. 657 Property(f3(c1)) | Property(f3(c2)) | - Situation(c1). [resolve(655,d,159,a),merge(e),unit_del(d,186)]. 658 Property(f3(c1)) | Property(f3(c2)). [resolve(657,c,160,a),merge(c)]. 659 Property(f3(c1)) | f3(c2) = f1(c2,L) | Situation(c2). [resolve(658,b,213,a)]. 660 Property(f3(c1)) | Situation(c2). [resolve(659,b,182,d),merge(d),unit_del(c,81),unit_del(d,84)]. 661 Property(f3(c1)) | Property(f1(c1,f4(c1))). [resolve(660,b,333,c),merge(b),unit_del(c,186)]. 894 Property(f3(c1)) | Actual(c1) | f1(c1,f4(c1)) = f1(c1,T). [resolve(634,c,661,b),merge(d)]. 899 Property(f3(c1)) | Actual(c1) | True(f4(c1),W) | - Situation(c1). [para(894(c,1),291(c,1)),merge(c),merge(d),unit_del(c,648)]. 914 Property(f3(c1)) | Actual(c1) | True(f4(c1),W). [resolve(899,d,160,a),merge(d)]. 916 Property(f3(c1)) | Actual(c1) | - Situation(c1). [resolve(914,c,94,d),merge(d),unit_del(c,80)]. 917 Property(f3(c1)) | Actual(c1). [resolve(916,c,160,a),merge(c)]. 918 Property(f3(c1)) | - Situation(c1) | - Situation(x) | Actual(x). [resolve(917,b,88,b)]. 922 Property(f3(c1)) | - Situation(c1). [resolve(918,c,660,b),merge(d),unit_del(c,186)]. 923 Property(f3(c1)). [resolve(922,b,160,a),merge(b)]. 924 Situation(c1) | f3(c1) = f1(c1,T). [back_unit_del(635),unit_del(b,923)]. 925 Situation(c1). [resolve(924,b,645,d),merge(c),unit_del(b,80),unit_del(c,83)]. 950 Actual(c1) | TrueIn(f4(c1),c1). [resolve(925,a,93,c),unit_del(a,80)]. 951 Actual(c1) | Encp(c1,f4(c1)). [resolve(950,b,139,b),merge(d),unit_del(b,80),unit_del(d,925)]. 952 Actual(c1) | VAC(f4(c1)) = f1(c1,f4(c1)). [resolve(951,b,142,b),merge(d),unit_del(b,80),unit_del(d,925)]. 953 Actual(c1) | Enc(c1,f1(c1,f4(c1))). [resolve(951,b,141,b),merge(d),unit_del(b,80),unit_del(d,925)]. 954 Actual(c1) | Property(f1(c1,f4(c1))). [resolve(951,b,140,b),merge(d),unit_del(b,80),unit_del(d,925)]. 959 Actual(c1) | - Property(f1(c1,f4(c1))) | f1(c1,f4(c1)) = f1(c1,T). [resolve(953,b,637,b),flip(c)]. 962 Property(f1(c1,f4(c1))) | - Situation(x) | Actual(x). [resolve(954,a,88,b),unit_del(b,925)]. 988 Actual(c1) | - Ex1At(f1(c1,f4(c1)),c1,W) | True(f4(c1),W). [para(952(b,1),154(b,1)),merge(e),unit_del(b,80),unit_del(e,925)]. 989 Property(f1(c1,f4(c1))) | Property(f3(c2)). [resolve(962,b,159,a),unit_del(b,186)]. 1014 Actual(c1) | f1(c1,f4(c1)) = f1(c1,T) | Property(f3(c2)). [resolve(959,b,989,a)]. 1017 Actual(c1) | Property(f3(c2)) | True(f4(c1),W). [para(1014(b,1),988(b,1)),merge(c),unit_del(c,648)]. 1019 Actual(c1) | Property(f3(c2)). [resolve(1017,c,94,d),merge(d),unit_del(c,80),unit_del(d,925)]. 1020 Property(f3(c2)) | - Situation(x) | Actual(x). [resolve(1019,a,88,b),unit_del(b,925)]. 1025 Property(f3(c2)). [resolve(1020,b,159,a),merge(c),unit_del(b,186)]. 1026 f3(c2) = f1(c2,L) | Situation(c2). [back_unit_del(213),unit_del(a,1025)]. 1027 Situation(c2). [resolve(1026,a,182,d),merge(c),unit_del(b,81),unit_del(c,84)]. 1029 Property(f1(c1,f4(c1))). [resolve(1027,a,962,b),unit_del(b,186)]. 1034 - Actual(c1). [ur(88,a,925,a,c,1027,a,d,186,a)]. 1048 f1(c1,f4(c1)) = f1(c1,T). [back_unit_del(959),unit_del(a,1034),unit_del(b,1029)]. 1050 True(f4(c1),W). [back_unit_del(988),demod(1048(6)),unit_del(a,1034),unit_del(b,648)]. 1056 $F. [ur(94,a,80,a,b,1034,a,c,925,a),unit_del(a,1050)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=437. Generated=2070. Kept=976. proofs=1. Usable=111. Sos=23. Demods=7. Denials=0. Limbo=0, Disabled=921. Hints=0. Megabytes=0.65. User_CPU=0.18, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13564 exit (max_proofs) Sat Jul 21 16:05:41 2007