============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3749 was started by zalta on mally, Wed Jun 14 17:09:30 2006 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= set(auto2). % set(auto2) -> set(auto). % set(auto) -> set(auto_inference). % set(auto_inference) -> set(predicate_elim). % set(auto_inference) -> assign(eq_defs, unfold). % set(auto) -> set(auto_limits). % set(auto_limits) -> assign(max_weight, 100). % set(auto_limits) -> assign(sos_limit, 10000). % set(auto2) -> set(fof_reduction). % set(auto2) -> assign(new_constants, 1). % set(auto2) -> assign(fold_denial_max, 3). % set(auto2) -> assign(max_weight, 200). % set(auto2) -> assign(nest_penalty, 1). % set(auto2) -> assign(skolem_penalty, 3). % set(auto2) -> assign(sk_constant_weight, 0). % set(auto2) -> assign(prop_atom_weight, 5). % set(auto2) -> set(sort_initial_sos). % set(auto2) -> assign(sos_limit, -1). % set(auto2) -> assign(lrs_ticks, 3000). % set(auto2) -> assign(max_megs, 400). % set(auto2) -> assign(stats, some). % set(auto2) -> clear(echo_input). % set(auto2) -> set(quiet). % set(auto2) -> clear(print_subproblems). % set(auto2) -> clear(print_initial_clauses). % set(auto2) -> clear(print_given). % formulas(sos). % not echoed (6 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <131,41>. Problem reduction (0.00 sec) gives one subproblem (<191,36>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 21 clauses. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. ============================== PROOF ================================= % Proof 1 at 0.06 (+ 0.01) seconds. % Length of proof is 81. % Level of proof is 32. % Maximum clause weight is 31. % Given clauses 193. 1 Situation(c1). [clausify]. 2 Situation(c2). [clausify]. 4 - Situation(x) | Object(x). [clausify]. 5 - Object(x) | - Situation(x) | Ex1At(A,x,W). [clausify]. 8 - Object(x) | - Proposition(y) | - TrueIn(y,x) | Encp(x,y). [clausify]. 9 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 12 - Object(x) | - Proposition(y) | - Encp(x,y) | Enc(x,f1(x,y)). [clausify]. 14 - Object(x) | - Proposition(y) | - Encp(x,y) | VAC(y) = f1(x,y). [clausify]. 15 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f2(x,y)). [clausify]. 16 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f2(x,y)) = y. [clausify]. 19 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 24 - Object(c1) | Ex1At(A,c1,W). [resolve(5,b,1,a)]. 25 - Object(c2) | Ex1At(A,c2,W). [resolve(5,b,2,a)]. 26 - Object(c1) | - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [resolve(15,b,1,a)]. 27 - Object(c2) | - Property(x) | - Enc(c2,x) | Proposition(f2(c2,x)). [resolve(15,b,2,a)]. 30 - Object(c1) | - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [resolve(16,b,1,a)]. 31 - Object(c2) | - Property(x) | - Enc(c2,x) | VAC(f2(c2,x)) = x. [resolve(16,b,2,a)]. 37 - Object(x) | - Proposition(y) | Enc(x,f1(x,y)) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(12,c,8,d)]. 38 - Object(x) | - Proposition(y) | VAC(y) = f1(x,y) | - Object(x) | - Proposition(y) | - TrueIn(y,x). [resolve(14,c,8,d)]. 39 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | - Object(x) | - Proposition(y) | TrueIn(y,x). [resolve(19,c,9,d)]. 43 c2 != c1. [clausify]. 44 - Proposition(x) | - TrueIn(x,c1) | TrueIn(x,c2). [clausify]. 45 - Proposition(x) | TrueIn(x,c1) | - TrueIn(x,c2). [clausify]. 46 - Ex1At(A,x,W) | - Ex1At(A,y,W) | Property(f4(x,y)) | y = x. [clausify]. 47 - Ex1At(A,x,W) | - Ex1At(A,y,W) | Enc(x,f4(x,y)) | Enc(y,f4(x,y)) | y = x. [clausify]. 48 - Ex1At(A,x,W) | - Ex1At(A,y,W) | - Enc(x,f4(x,y)) | - Enc(y,f4(x,y)) | y = x. [clausify]. 49 Object(c1). [resolve(4,a,1,a)]. 50 Object(c2). [resolve(4,a,2,a)]. 51 Ex1At(A,c1,W). [copy(24),unit_del(a,49)]. 52 Ex1At(A,c2,W). [copy(25),unit_del(a,50)]. 53 - Property(x) | - Enc(c1,x) | Proposition(f2(c1,x)). [copy(26),unit_del(a,49)]. 54 - Property(x) | - Enc(c2,x) | Proposition(f2(c2,x)). [copy(27),unit_del(a,50)]. 57 - Property(x) | - Enc(c1,x) | VAC(f2(c1,x)) = x. [copy(30),unit_del(a,49)]. 58 - Property(x) | - Enc(c2,x) | VAC(f2(c2,x)) = x. [copy(31),unit_del(a,50)]. 64 - Object(x) | - Proposition(y) | Enc(x,f1(x,y)) | - TrueIn(y,x). [copy(37),merge(d),merge(e)]. 65 - Object(x) | - Proposition(y) | f1(x,y) = VAC(y) | - TrueIn(y,x). [copy(38),flip(c),merge(d),merge(e)]. 66 - Object(x) | - Proposition(y) | - Property(z) | VAC(y) != z | - Enc(x,z) | TrueIn(y,x). [copy(39),merge(f),merge(g)]. 70 - Ex1At(A,x,W) | - Enc(x,f4(x,c1)) | - Enc(c1,f4(x,c1)) | c1 = x. [resolve(51,a,48,b)]. 72 - Ex1At(A,x,W) | Enc(x,f4(x,c1)) | Enc(c1,f4(x,c1)) | c1 = x. [resolve(51,a,47,b)]. 74 - Ex1At(A,x,W) | Property(f4(x,c1)) | c1 = x. [resolve(51,a,46,b)]. 86 Property(f4(c2,c1)). [resolve(74,a,52,a),flip(b),unit_del(b,43)]. 88 - Enc(c2,f4(c2,c1)) | - Enc(c1,f4(c2,c1)). [resolve(70,a,52,a),flip(c),unit_del(c,43)]. 90 Enc(c2,f4(c2,c1)) | Enc(c1,f4(c2,c1)). [resolve(72,a,52,a),flip(c),unit_del(c,43)]. 91 Enc(c1,f4(c2,c1)) | VAC(f2(c2,f4(c2,c1))) = f4(c2,c1). [resolve(90,a,58,b),unit_del(b,86)]. 92 Enc(c1,f4(c2,c1)) | Proposition(f2(c2,f4(c2,c1))). [resolve(90,a,54,b),unit_del(b,86)]. 93 Proposition(f2(c2,f4(c2,c1))) | VAC(f2(c1,f4(c2,c1))) = f4(c2,c1). [resolve(92,a,57,b),unit_del(b,86)]. 94 Proposition(f2(c2,f4(c2,c1))) | Proposition(f2(c1,f4(c2,c1))). [resolve(92,a,53,b),unit_del(b,86)]. 103 Enc(c1,f4(c2,c1)) | - Object(x) | - Proposition(f2(c2,f4(c2,c1))) | - Enc(x,f4(c2,c1)) | TrueIn(f2(c2,f4(c2,c1)),x). [resolve(91,b,66,d),unit_del(d,86)]. 123 Proposition(f2(c2,f4(c2,c1))) | - Object(x) | - Proposition(f2(c1,f4(c2,c1))) | - Enc(x,f4(c2,c1)) | TrueIn(f2(c1,f4(c2,c1)),x). [resolve(93,b,66,d),unit_del(d,86)]. 158 Enc(c1,f4(c2,c1)) | - Proposition(f2(c2,f4(c2,c1))) | TrueIn(f2(c2,f4(c2,c1)),c2). [resolve(103,d,90,a),merge(e),unit_del(b,50)]. 160 Enc(c1,f4(c2,c1)) | TrueIn(f2(c2,f4(c2,c1)),c2) | Proposition(f2(c1,f4(c2,c1))). [resolve(158,b,94,a)]. 163 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | - Proposition(f2(c2,f4(c2,c1))) | TrueIn(f2(c2,f4(c2,c1)),c1). [resolve(160,b,45,c)]. 164 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | TrueIn(f2(c2,f4(c2,c1)),c1). [resolve(163,c,94,a),merge(d)]. 165 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | - Proposition(f2(c2,f4(c2,c1))) | VAC(f2(c2,f4(c2,c1))) = f1(c1,f2(c2,f4(c2,c1))). [resolve(164,c,65,d),flip(e),unit_del(c,49)]. 166 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | - Proposition(f2(c2,f4(c2,c1))) | Enc(c1,f1(c1,f2(c2,f4(c2,c1)))). [resolve(164,c,64,d),unit_del(c,49)]. 180 Proposition(f2(c2,f4(c2,c1))) | - Proposition(f2(c1,f4(c2,c1))) | TrueIn(f2(c1,f4(c2,c1)),c1). [resolve(123,d,92,a),merge(e),unit_del(b,49)]. 189 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | Enc(c1,f1(c1,f2(c2,f4(c2,c1)))). [resolve(166,c,94,a),merge(d)]. 249 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | VAC(f2(c2,f4(c2,c1))) = f1(c1,f2(c2,f4(c2,c1))). [resolve(165,c,94,a),merge(d)]. 261 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))) | f1(c1,f2(c2,f4(c2,c1))) = f4(c2,c1). [para(249(c,1),91(b,1)),merge(c)]. 269 Enc(c1,f4(c2,c1)) | Proposition(f2(c1,f4(c2,c1))). [para(261(c,1),189(c,2)),merge(c),merge(d),merge(e)]. 271 Proposition(f2(c1,f4(c2,c1))). [resolve(269,a,53,b),merge(c),unit_del(b,86)]. 275 Proposition(f2(c2,f4(c2,c1))) | TrueIn(f2(c1,f4(c2,c1)),c1). [back_unit_del(180),unit_del(b,271)]. 292 Proposition(f2(c2,f4(c2,c1))) | TrueIn(f2(c1,f4(c2,c1)),c2). [resolve(275,b,44,b),unit_del(b,271)]. 293 Proposition(f2(c2,f4(c2,c1))) | VAC(f2(c1,f4(c2,c1))) = f1(c2,f2(c1,f4(c2,c1))). [resolve(292,b,65,d),flip(d),unit_del(b,50),unit_del(c,271)]. 294 Proposition(f2(c2,f4(c2,c1))) | Enc(c2,f1(c2,f2(c1,f4(c2,c1)))). [resolve(292,b,64,d),unit_del(b,50),unit_del(c,271)]. 327 Proposition(f2(c2,f4(c2,c1))) | f1(c2,f2(c1,f4(c2,c1))) = f4(c2,c1). [para(293(b,1),93(b,1)),merge(b)]. 335 Proposition(f2(c2,f4(c2,c1))) | Enc(c2,f4(c2,c1)). [para(327(b,1),294(b,2)),merge(b)]. 338 Proposition(f2(c2,f4(c2,c1))). [resolve(335,b,54,b),merge(c),unit_del(b,86)]. 342 Enc(c1,f4(c2,c1)) | TrueIn(f2(c2,f4(c2,c1)),c2). [back_unit_del(158),unit_del(b,338)]. 357 Enc(c1,f4(c2,c1)) | TrueIn(f2(c2,f4(c2,c1)),c1). [resolve(342,b,45,c),unit_del(b,338)]. 358 Enc(c1,f4(c2,c1)) | VAC(f2(c2,f4(c2,c1))) = f1(c1,f2(c2,f4(c2,c1))). [resolve(357,b,65,d),flip(d),unit_del(b,49),unit_del(c,338)]. 359 Enc(c1,f4(c2,c1)) | Enc(c1,f1(c1,f2(c2,f4(c2,c1)))). [resolve(357,b,64,d),unit_del(b,49),unit_del(c,338)]. 395 Enc(c1,f4(c2,c1)) | f1(c1,f2(c2,f4(c2,c1))) = f4(c2,c1). [para(358(b,1),91(b,1)),merge(b)]. 402 Enc(c1,f4(c2,c1)). [para(395(b,1),359(b,2)),merge(b),merge(c)]. 403 - Enc(c2,f4(c2,c1)). [back_unit_del(88),unit_del(b,402)]. 404 VAC(f2(c1,f4(c2,c1))) = f4(c2,c1). [resolve(402,a,57,b),unit_del(a,86)]. 408 - Object(x) | - Enc(x,f4(c2,c1)) | TrueIn(f2(c1,f4(c2,c1)),x). [resolve(404,a,66,d),unit_del(b,271),unit_del(c,86)]. 415 TrueIn(f2(c1,f4(c2,c1)),c1). [resolve(408,b,402,a),unit_del(a,49)]. 418 TrueIn(f2(c1,f4(c2,c1)),c2). [resolve(415,a,44,b),unit_del(a,271)]. 419 f1(c2,f2(c1,f4(c2,c1))) = f4(c2,c1). [resolve(418,a,65,d),demod(404(21)),unit_del(a,50),unit_del(b,271)]. 420 $F. [resolve(418,a,64,d),demod(419(16)),unit_del(a,50),unit_del(b,271),unit_del(c,403)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=193. Generated=669. Kept=377. proofs=1. Usable=103. Sos=26. Demods=3. Denials=0. Limbo=1, Disabled=289. Hints=0. Megabytes=0.41. User_CPU=0.06, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3749 exit (max_proofs) Wed Jun 14 17:09:30 2006