============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3747 was started by zalta on mally, Wed Jun 14 17:09:17 2006 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= op(300,prefix,~). 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 (12 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 36 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.86 (+ 0.02) seconds. % Length of proof is 144. % Level of proof is 54. % Maximum clause weight is 32. % Given clauses 604. 1 Point(W). [clausify]. 2 World(c1). [clausify]. 3 World(c2). [clausify]. 4 Actual(c1). [clausify]. 5 Actual(c2). [clausify]. 7 - Point(x) | - Proposition(y) | - True(~ y,x) | - True(y,x). [clausify]. 8 - World(x) | Object(x). [clausify]. 9 - World(x) | Maximal1(x). [clausify]. 11 - Object(x) | - Actual(x) | Situation(x). [clausify]. 13 - Object(x) | - Situation(x) | Ex1At(A,x,W). [clausify]. 16 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 17 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(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]. 29 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)). [clausify]. 30 - Object(x) | - Maximal1(x) | - Proposition(y) | TrueIn(y,x) | TrueIn(~ y,x). [clausify]. 31 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y. [clausify]. 34 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 41 Maximal1(c1). [resolve(9,a,2,a)]. 42 Maximal1(c2). [resolve(9,a,3,a)]. 43 - Object(c1) | Situation(c1). [resolve(11,b,4,a)]. 44 - Object(c2) | Situation(c2). [resolve(11,b,5,a)]. 45 - Object(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,W). [resolve(27,b,4,a)]. 46 - Object(c2) | - Proposition(x) | - TrueIn(x,c2) | True(x,W). [resolve(27,b,5,a)]. 54 - Object(c1) | - Proposition(x) | TrueIn(x,c1) | TrueIn(~ x,c1). [resolve(41,a,30,b)]. 56 - Object(c2) | - Proposition(x) | TrueIn(x,c2) | TrueIn(~ x,c2). [resolve(42,a,30,b)]. 63 - Object(c1) | - Object(c1) | Ex1At(A,c1,W). [resolve(43,b,13,b)]. 64 - Object(c1) | - Object(c1) | - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [resolve(43,b,29,b)]. 65 - Object(c1) | - Object(c1) | - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [resolve(43,b,31,b)]. 66 - Object(c2) | - Object(c2) | Ex1At(A,c2,W). [resolve(44,b,13,b)]. 67 - Object(c2) | - Object(c2) | - Property(x) | - Enc(c2,x) | Proposition(f2(c2,x)). [resolve(44,b,29,b)]. 68 - Object(c2) | - Object(c2) | - Property(x) | - Enc(c2,x) | VAC(f2(c2,x)) = x. [resolve(44,b,31,b)]. 100 - Object(x) | - Proposition(y) | Enc(x,f1(x,y)) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(25,c,16,d)]. 101 - Object(x) | - Proposition(y) | VAC(y) = f1(x,y) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(28,c,16,d)]. 102 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | - Object(x) | - Proposition(y) | TrueIn(y,x). [resolve(34,c,17,d)]. 105 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | - Object(x) | - Proposition(y) | VAC(y) = f1(x,y). [resolve(34,c,28,c)]. 106 c2 != c1. [clausify]. 107 - Proposition(x) | Proposition(~ x). [clausify]. 108 - Ex1At(A,x,W) | - Ex1At(A,y,W) | Property(f6(x,y)) | y = x. [clausify]. 109 - Ex1At(A,x,W) | - Ex1At(A,y,W) | Enc(x,f6(x,y)) | Enc(y,f6(x,y)) | y = x. [clausify]. 110 - Ex1At(A,x,W) | - Ex1At(A,y,W) | - Enc(x,f6(x,y)) | - Enc(y,f6(x,y)) | y = x. [clausify]. 111 - Proposition(x) | - True(~ x,W) | - True(x,W). [resolve(7,a,1,a)]. 113 Object(c1). [resolve(8,a,2,a)]. 114 Object(c2). [resolve(8,a,3,a)]. 115 - Proposition(x) | - TrueIn(x,c1) | True(x,W). [copy(45),unit_del(a,113)]. 116 - Proposition(x) | - TrueIn(x,c2) | True(x,W). [copy(46),unit_del(a,114)]. 117 - Proposition(x) | TrueIn(x,c1) | TrueIn(~ x,c1). [copy(54),unit_del(a,113)]. 118 - Proposition(x) | TrueIn(x,c2) | TrueIn(~ x,c2). [copy(56),unit_del(a,114)]. 125 Ex1At(A,c1,W). [copy(63),merge(b),unit_del(a,113)]. 126 - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [copy(64),merge(b),unit_del(a,113)]. 127 - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [copy(65),merge(b),unit_del(a,113)]. 128 Ex1At(A,c2,W). [copy(66),merge(b),unit_del(a,114)]. 129 - Property(x) | - Enc(c2,x) | Proposition(f2(c2,x)). [copy(67),merge(b),unit_del(a,114)]. 130 - Property(x) | - Enc(c2,x) | VAC(f2(c2,x)) = x. [copy(68),merge(b),unit_del(a,114)]. 150 - Object(x) | - Proposition(y) | Enc(x,f1(x,y)) | - TrueIn(y,x). [copy(100),merge(d),merge(e)]. 151 - Object(x) | - Proposition(y) | f1(x,y) = VAC(y) | - TrueIn(y,x). [copy(101),flip(c),merge(d),merge(e)]. 152 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | TrueIn(y,x). [copy(102),merge(f),merge(g)]. 155 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | f1(x,y) = VAC(y). [copy(105),flip(h),merge(f),merge(g)]. 162 - Ex1At(A,x,W) | - Enc(x,f6(x,c1)) | - Enc(c1,f6(x,c1)) | c1 = x. [resolve(125,a,110,b)]. 164 - Ex1At(A,x,W) | Enc(x,f6(x,c1)) | Enc(c1,f6(x,c1)) | c1 = x. [resolve(125,a,109,b)]. 166 - Ex1At(A,x,W) | Property(f6(x,c1)) | c1 = x. [resolve(125,a,108,b)]. 178 Property(f6(c2,c1)). [resolve(166,a,128,a),flip(b),unit_del(b,106)]. 180 - Enc(c2,f6(c2,c1)) | - Enc(c1,f6(c2,c1)). [resolve(162,a,128,a),flip(c),unit_del(c,106)]. 182 Enc(c2,f6(c2,c1)) | Enc(c1,f6(c2,c1)). [resolve(164,a,128,a),flip(c),unit_del(c,106)]. 183 Enc(c1,f6(c2,c1)) | VAC(f2(c2,f6(c2,c1))) = f6(c2,c1). [resolve(182,a,130,b),unit_del(b,178)]. 184 Enc(c1,f6(c2,c1)) | Proposition(f2(c2,f6(c2,c1))). [resolve(182,a,129,b),unit_del(b,178)]. 185 Proposition(f2(c2,f6(c2,c1))) | VAC(f2(c1,f6(c2,c1))) = f6(c2,c1). [resolve(184,a,127,b),unit_del(b,178)]. 186 Proposition(f2(c2,f6(c2,c1))) | Proposition(f2(c1,f6(c2,c1))). [resolve(184,a,126,b),unit_del(b,178)]. 187 Enc(c1,f6(c2,c1)) | - Object(x) | - Proposition(f2(c2,f6(c2,c1))) | - Enc(x,f6(c2,c1)) | f1(x,f2(c2,f6(c2,c1))) = VAC(f2(c2,f6(c2,c1))). [resolve(183,b,155,d),unit_del(d,178)]. 190 Enc(c1,f6(c2,c1)) | - Object(x) | - Proposition(f2(c2,f6(c2,c1))) | - Enc(x,f6(c2,c1)) | TrueIn(f2(c2,f6(c2,c1)),x). [resolve(183,b,152,d),unit_del(d,178)]. 237 Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c1) | TrueIn(~ f2(c2,f6(c2,c1)),c1). [resolve(186,a,117,a)]. 239 Proposition(f2(c1,f6(c2,c1))) | Proposition(~ f2(c2,f6(c2,c1))). [resolve(186,a,107,a)]. 255 Proposition(f2(c2,f6(c2,c1))) | - Object(x) | - Proposition(f2(c1,f6(c2,c1))) | - Enc(x,f6(c2,c1)) | TrueIn(f2(c1,f6(c2,c1)),x). [resolve(185,b,152,d),unit_del(d,178)]. 333 Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c1) | - Proposition(~ f2(c2,f6(c2,c1))) | True(~ f2(c2,f6(c2,c1)),W). [resolve(237,c,115,b)]. 354 Enc(c1,f6(c2,c1)) | - Proposition(f2(c2,f6(c2,c1))) | VAC(f2(c2,f6(c2,c1))) = f1(c2,f2(c2,f6(c2,c1))). [resolve(187,d,182,a),flip(d),merge(e),unit_del(b,114)]. 355 Enc(c1,f6(c2,c1)) | - Proposition(f2(c2,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c2). [resolve(190,d,182,a),merge(e),unit_del(b,114)]. 356 Enc(c1,f6(c2,c1)) | TrueIn(f2(c2,f6(c2,c1)),c2) | Proposition(f2(c1,f6(c2,c1))). [resolve(355,b,186,a)]. 358 TrueIn(f2(c2,f6(c2,c1)),c2) | Proposition(f2(c1,f6(c2,c1))). [resolve(356,a,126,b),merge(d),unit_del(c,178)]. 362 Proposition(f2(c1,f6(c2,c1))) | - Proposition(f2(c2,f6(c2,c1))) | True(f2(c2,f6(c2,c1)),W). [resolve(358,a,116,b)]. 364 Proposition(f2(c1,f6(c2,c1))) | True(f2(c2,f6(c2,c1)),W). [resolve(362,b,186,a),merge(c)]. 399 Proposition(f2(c2,f6(c2,c1))) | - Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c1,f6(c2,c1)),c1). [resolve(255,d,184,a),merge(e),unit_del(b,113)]. 431 Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c1) | True(~ f2(c2,f6(c2,c1)),W). [resolve(333,c,239,b),merge(d)]. 432 Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c1) | - Proposition(f2(c2,f6(c2,c1))) | - True(f2(c2,f6(c2,c1)),W). [resolve(431,c,111,b)]. 433 Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c1) | - Proposition(f2(c2,f6(c2,c1))). [resolve(432,d,364,b),merge(d)]. 434 Proposition(f2(c1,f6(c2,c1))) | TrueIn(f2(c2,f6(c2,c1)),c1). [resolve(433,c,186,a),merge(c)]. 435 Proposition(f2(c1,f6(c2,c1))) | - Proposition(f2(c2,f6(c2,c1))) | VAC(f2(c2,f6(c2,c1))) = f1(c1,f2(c2,f6(c2,c1))). [resolve(434,b,151,d),flip(d),unit_del(b,113)]. 436 Proposition(f2(c1,f6(c2,c1))) | - Proposition(f2(c2,f6(c2,c1))) | Enc(c1,f1(c1,f2(c2,f6(c2,c1)))). [resolve(434,b,150,d),unit_del(b,113)]. 460 Proposition(f2(c1,f6(c2,c1))) | Enc(c1,f1(c1,f2(c2,f6(c2,c1)))). [resolve(436,b,186,a),merge(c)]. 621 Proposition(f2(c1,f6(c2,c1))) | VAC(f2(c2,f6(c2,c1))) = f1(c1,f2(c2,f6(c2,c1))). [resolve(435,b,186,a),merge(c)]. 641 Proposition(f2(c1,f6(c2,c1))) | Enc(c1,f6(c2,c1)) | f1(c1,f2(c2,f6(c2,c1))) = f6(c2,c1). [para(621(b,1),183(b,1))]. 653 Proposition(f2(c1,f6(c2,c1))) | Enc(c1,f6(c2,c1)). [para(641(c,1),460(b,2)),merge(c),merge(d)]. 655 Proposition(f2(c1,f6(c2,c1))). [resolve(653,b,126,b),merge(c),unit_del(b,178)]. 656 Proposition(f2(c2,f6(c2,c1))) | TrueIn(f2(c1,f6(c2,c1)),c1). [back_unit_del(399),unit_del(b,655)]. 684 TrueIn(f2(c1,f6(c2,c1)),c2) | TrueIn(~ f2(c1,f6(c2,c1)),c2). [resolve(655,a,118,a)]. 687 Proposition(~ f2(c1,f6(c2,c1))). [resolve(655,a,107,a)]. 699 Proposition(f2(c2,f6(c2,c1))) | True(f2(c1,f6(c2,c1)),W). [resolve(656,b,115,b),unit_del(b,655)]. 707 TrueIn(f2(c1,f6(c2,c1)),c2) | True(~ f2(c1,f6(c2,c1)),W). [resolve(684,b,116,b),unit_del(b,687)]. 716 TrueIn(f2(c1,f6(c2,c1)),c2) | - True(f2(c1,f6(c2,c1)),W). [resolve(707,b,111,b),unit_del(b,655)]. 717 TrueIn(f2(c1,f6(c2,c1)),c2) | Proposition(f2(c2,f6(c2,c1))). [resolve(716,b,699,b)]. 718 Proposition(f2(c2,f6(c2,c1))) | VAC(f2(c1,f6(c2,c1))) = f1(c2,f2(c1,f6(c2,c1))). [resolve(717,a,151,d),flip(d),unit_del(b,114),unit_del(c,655)]. 719 Proposition(f2(c2,f6(c2,c1))) | Enc(c2,f1(c2,f2(c1,f6(c2,c1)))). [resolve(717,a,150,d),unit_del(b,114),unit_del(c,655)]. 916 Proposition(f2(c2,f6(c2,c1))) | f1(c2,f2(c1,f6(c2,c1))) = f6(c2,c1). [para(718(b,1),185(b,1)),merge(b)]. 924 Proposition(f2(c2,f6(c2,c1))) | Enc(c2,f6(c2,c1)). [para(916(b,1),719(b,2)),merge(b)]. 927 Proposition(f2(c2,f6(c2,c1))). [resolve(924,b,129,b),merge(c),unit_del(b,178)]. 930 Enc(c1,f6(c2,c1)) | TrueIn(f2(c2,f6(c2,c1)),c2). [back_unit_del(355),unit_del(b,927)]. 931 Enc(c1,f6(c2,c1)) | VAC(f2(c2,f6(c2,c1))) = f1(c2,f2(c2,f6(c2,c1))). [back_unit_del(354),unit_del(b,927)]. 959 TrueIn(f2(c2,f6(c2,c1)),c1) | TrueIn(~ f2(c2,f6(c2,c1)),c1). [resolve(927,a,117,a)]. 961 Proposition(~ f2(c2,f6(c2,c1))). [resolve(927,a,107,a)]. 966 TrueIn(f2(c2,f6(c2,c1)),c2) | VAC(f2(c1,f6(c2,c1))) = f6(c2,c1). [resolve(930,a,127,b),unit_del(b,178)]. 982 TrueIn(f2(c2,f6(c2,c1)),c1) | True(~ f2(c2,f6(c2,c1)),W). [resolve(959,b,115,b),unit_del(b,961)]. 986 TrueIn(f2(c2,f6(c2,c1)),c2) | - Object(x) | - Enc(x,f6(c2,c1)) | TrueIn(f2(c1,f6(c2,c1)),x). [resolve(966,b,152,d),unit_del(c,655),unit_del(d,178)]. 1014 TrueIn(f2(c2,f6(c2,c1)),c1) | - True(f2(c2,f6(c2,c1)),W). [resolve(982,b,111,b),unit_del(b,927)]. 1045 TrueIn(f2(c2,f6(c2,c1)),c2) | TrueIn(f2(c1,f6(c2,c1)),c1). [resolve(986,c,930,a),merge(d),unit_del(b,113)]. 1049 TrueIn(f2(c1,f6(c2,c1)),c1) | True(f2(c2,f6(c2,c1)),W). [resolve(1045,a,116,b),unit_del(b,927)]. 1050 TrueIn(f2(c1,f6(c2,c1)),c1) | TrueIn(f2(c2,f6(c2,c1)),c1). [resolve(1049,b,1014,b)]. 1051 TrueIn(f2(c1,f6(c2,c1)),c1) | VAC(f2(c2,f6(c2,c1))) = f1(c1,f2(c2,f6(c2,c1))). [resolve(1050,b,151,d),flip(d),unit_del(b,113),unit_del(c,927)]. 1052 TrueIn(f2(c1,f6(c2,c1)),c1) | Enc(c1,f1(c1,f2(c2,f6(c2,c1)))). [resolve(1050,b,150,d),unit_del(b,113),unit_del(c,927)]. 1157 Enc(c1,f6(c2,c1)) | f1(c2,f2(c2,f6(c2,c1))) = f6(c2,c1). [para(931(b,1),183(b,1)),merge(b)]. 1350 TrueIn(f2(c1,f6(c2,c1)),c1) | Enc(c1,f6(c2,c1)) | f1(c1,f2(c2,f6(c2,c1))) = f6(c2,c1). [para(1051(b,1),183(b,1))]. 1363 TrueIn(f2(c1,f6(c2,c1)),c1) | Enc(c1,f6(c2,c1)). [para(1350(c,1),1052(b,2)),merge(c),merge(d)]. 1364 TrueIn(f2(c1,f6(c2,c1)),c1) | VAC(f2(c1,f6(c2,c1))) = f6(c2,c1). [resolve(1363,b,127,b),unit_del(b,178)]. 1368 TrueIn(f2(c1,f6(c2,c1)),c1) | - Object(x) | - Enc(x,f6(c2,c1)) | TrueIn(f2(c1,f6(c2,c1)),x). [resolve(1364,b,152,d),unit_del(c,655),unit_del(d,178)]. 1391 TrueIn(f2(c1,f6(c2,c1)),c1) | - Enc(c1,f6(c2,c1)). [factor(1368,a,d),unit_del(b,113)]. 1394 TrueIn(f2(c1,f6(c2,c1)),c1). [resolve(1391,b,1363,b),merge(b)]. 1396 VAC(f2(c1,f6(c2,c1))) = f1(c1,f2(c1,f6(c2,c1))). [resolve(1394,a,151,d),flip(c),unit_del(a,113),unit_del(b,655)]. 1399 True(f2(c1,f6(c2,c1)),W). [resolve(1394,a,115,b),unit_del(a,655)]. 1415 TrueIn(f2(c2,f6(c2,c1)),c2) | f1(c1,f2(c1,f6(c2,c1))) = f6(c2,c1). [back_demod(966),demod(1396(13))]. 1420 TrueIn(f2(c1,f6(c2,c1)),c2). [back_unit_del(716),unit_del(b,1399)]. 1421 f1(c2,f2(c1,f6(c2,c1))) = f1(c1,f2(c1,f6(c2,c1))). [resolve(1420,a,151,d),demod(1396(21)),unit_del(a,114),unit_del(b,655)]. 1422 Enc(c2,f1(c1,f2(c1,f6(c2,c1)))). [resolve(1420,a,150,d),demod(1421(16)),unit_del(a,114),unit_del(b,655)]. 1509 TrueIn(f2(c2,f6(c2,c1)),c2) | Enc(c2,f6(c2,c1)). [para(1415(b,1),1422(a,2))]. 1513 TrueIn(f2(c2,f6(c2,c1)),c2) | - Enc(c1,f6(c2,c1)). [resolve(1509,b,180,a)]. 1520 TrueIn(f2(c2,f6(c2,c1)),c2). [resolve(1513,b,930,a),merge(b)]. 1521 VAC(f2(c2,f6(c2,c1))) = f1(c2,f2(c2,f6(c2,c1))). [resolve(1520,a,151,d),flip(c),unit_del(a,114),unit_del(b,927)]. 1524 True(f2(c2,f6(c2,c1)),W). [resolve(1520,a,116,b),unit_del(a,927)]. 1537 TrueIn(f2(c2,f6(c2,c1)),c1). [back_unit_del(1014),unit_del(b,1524)]. 1542 f1(c2,f2(c2,f6(c2,c1))) = f1(c1,f2(c2,f6(c2,c1))). [resolve(1537,a,151,d),demod(1521(21)),flip(c),unit_del(a,113),unit_del(b,927)]. 1543 Enc(c1,f1(c1,f2(c2,f6(c2,c1)))). [resolve(1537,a,150,d),unit_del(a,113),unit_del(b,927)]. 1556 Enc(c1,f6(c2,c1)) | f1(c1,f2(c2,f6(c2,c1))) = f6(c2,c1). [back_demod(1157),demod(1542(12))]. 1627 Enc(c1,f6(c2,c1)). [para(1556(b,1),1543(a,2)),merge(b)]. 1628 - Enc(c2,f6(c2,c1)). [back_unit_del(180),unit_del(b,1627)]. 1630 f1(c1,f2(c1,f6(c2,c1))) = f6(c2,c1). [resolve(1627,a,127,b),demod(1396(10)),unit_del(a,178)]. 1658 $F. [back_demod(1422),demod(1630(8)),unit_del(a,1628)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=604. Generated=2312. Kept=1552. proofs=1. Usable=262. Sos=166. Demods=20. Denials=0. Limbo=28, Disabled=1193. Hints=0. Megabytes=2.04. User_CPU=0.86, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3747 exit (max_proofs) Wed Jun 14 17:09:17 2006