============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3768 was started by zalta on mally, Wed Jun 14 17:11:48 2006 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= set(auto2). % set(auto2) -> set(auto). % set(auto) -> set(auto_inference). % set(auto_inference) -> set(predicate_elim). % set(auto_inference) -> assign(eq_defs, unfold). % set(auto) -> set(auto_limits). % set(auto_limits) -> assign(max_weight, 100). % set(auto_limits) -> assign(sos_limit, 10000). % set(auto2) -> set(fof_reduction). % set(auto2) -> assign(new_constants, 1). % set(auto2) -> assign(fold_denial_max, 3). % set(auto2) -> assign(max_weight, 200). % set(auto2) -> assign(nest_penalty, 1). % set(auto2) -> assign(skolem_penalty, 3). % set(auto2) -> assign(sk_constant_weight, 0). % set(auto2) -> assign(prop_atom_weight, 5). % set(auto2) -> set(sort_initial_sos). % set(auto2) -> assign(sos_limit, -1). % set(auto2) -> assign(lrs_ticks, 3000). % set(auto2) -> assign(max_megs, 400). % set(auto2) -> assign(stats, some). % set(auto2) -> clear(echo_input). % set(auto2) -> set(quiet). % set(auto2) -> clear(print_subproblems). % set(auto2) -> clear(print_initial_clauses). % set(auto2) -> clear(print_given). clear(fof_reduction). % formulas(sos). % not echoed (5 formulas) ============================== end of input ========================== ============================== 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.10 (+ 0.01) seconds. % Length of proof is 108. % Level of proof is 27. % Maximum clause weight is 21. % Given clauses 263. 1 Situation(c1). [clausify]. 2 Situation(c2). [clausify]. 6 - Situation(x) | Object(x). [clausify]. 7 - Object(x) | - Situation(x) | Ex1(A,x,W). [clausify]. 24 - Object(c1) | Ex1(A,c1,W). [resolve(7,b,1,a)]. 25 - Object(c2) | Ex1(A,c2,W). [resolve(7,b,2,a)]. 36 c2 = c1 | PartOf(c1,c2). [clausify]. 37 c2 = c1 | PartOf(c2,c1). [clausify]. 38 c2 != c1 | - PartOf(c1,c2) | - PartOf(c2,c1). [clausify]. 41 - Object(x) | - Object(y) | - PartOf(x,y) | - Property(z) | - Enc(x,z) | Enc(y,z). [clausify]. 42 - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f4(x,y)) | y = x. [clausify]. 43 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f3(x,y)). [clausify]. 44 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f3(x,y)). [clausify]. 45 - Object(x) | - Object(y) | PartOf(x,y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(y,f3(x,y)). [clausify]. 46 - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f4(x,y)) | Enc(y,f4(x,y)) | y = x. [clausify]. 47 - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f4(x,y)) | - Enc(y,f4(x,y)) | y = x. [clausify]. 48 Object(c1). [resolve(6,a,1,a)]. 49 Object(c2). [resolve(6,a,2,a)]. 50 Ex1(A,c1,W). [copy(24),unit_del(a,48)]. 51 Ex1(A,c2,W). [copy(25),unit_del(a,49)]. 63 - Object(x) | PartOf(x,x) | - Ex1(A,x,W) | Property(f3(x,x)). [factor(43,a,b),merge(d)]. 64 - Object(x) | PartOf(x,x) | - Ex1(A,x,W) | Enc(x,f3(x,x)). [factor(44,a,b),merge(d)]. 65 - Object(x) | PartOf(x,x) | - Ex1(A,x,W) | - Enc(x,f3(x,x)). [factor(45,a,b),merge(d)]. 67 PartOf(c2,c1) | c2 != c1 | - PartOf(c1,c2) | - PartOf(c1,c1). [para(37(a,1),38(c,1))]. 69 - Ex1(A,x,W) | - Enc(c1,f4(c1,x)) | - Enc(x,f4(c1,x)) | c1 = x. [resolve(50,a,47,a),flip(d)]. 71 - Ex1(A,x,W) | Enc(c1,f4(c1,x)) | Enc(x,f4(c1,x)) | c1 = x. [resolve(50,a,46,a),flip(d)]. 73 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | - Enc(x,f3(c1,x)). [resolve(50,a,45,d),unit_del(a,48)]. 75 - Object(x) | PartOf(c1,x) | - Ex1(A,x,W) | Enc(c1,f3(c1,x)). [resolve(50,a,44,d),unit_del(a,48)]. 79 - Ex1(A,x,W) | Property(f4(c1,x)) | c1 = x. [resolve(50,a,42,a),flip(c)]. 96 PartOf(c2,c2) | Property(f3(c2,c2)). [resolve(63,c,51,a),unit_del(a,49)]. 98 PartOf(c2,c2) | Enc(c2,f3(c2,c2)). [resolve(64,c,51,a),unit_del(a,49)]. 99 PartOf(c1,c1) | Enc(c1,f3(c1,c1)). [resolve(64,c,50,a),unit_del(a,48)]. 100 PartOf(c2,c2) | - Enc(c2,f3(c2,c2)). [resolve(65,c,51,a),unit_del(a,49)]. 101 PartOf(c1,c1) | - Enc(c1,f3(c1,c1)). [resolve(65,c,50,a),unit_del(a,48)]. 104 PartOf(c1,c2) | Property(f3(c2,c2)). [para(36(a,1),96(a,1)),merge(b)]. 105 PartOf(c2,c1) | Property(f3(c2,c2)). [para(37(a,1),96(a,2)),merge(b)]. 106 PartOf(c1,c2) | Enc(c2,f3(c2,c2)). [para(36(a,1),98(a,1)),merge(b)]. 107 PartOf(c2,c1) | Enc(c2,f3(c2,c2)). [para(37(a,1),98(a,2)),merge(b)]. 108 PartOf(c2,c1) | - PartOf(c1,c2) | - PartOf(c1,c1). [resolve(67,b,37,a),merge(d)]. 120 Property(f3(c2,c2)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(104,a,41,c),unit_del(b,48),unit_del(c,49)]. 121 Property(f3(c2,c2)) | - Property(x) | - Enc(c2,x) | Enc(c1,x). [resolve(105,a,41,c),unit_del(b,49),unit_del(c,48)]. 122 Enc(c2,f3(c2,c2)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(106,a,41,c),unit_del(b,48),unit_del(c,49)]. 123 Enc(c2,f3(c2,c2)) | - Property(f3(c2,c2)) | - Enc(c1,f3(c2,c2)). [factor(122,a,d)]. 124 Enc(c2,f3(c2,c2)) | - Property(x) | - Enc(c2,x) | Enc(c1,x). [resolve(107,a,41,c),unit_del(b,49),unit_del(c,48)]. 125 - Enc(c1,f4(c1,c2)) | - Enc(c2,f4(c1,c2)) | c2 = c1. [resolve(69,a,51,a),flip(c)]. 126 PartOf(c2,c1) | - PartOf(c1,c1). [para(37(a,1),108(b,2)),merge(b),merge(d)]. 138 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | c2 = c1. [resolve(71,a,51,a),flip(c)]. 146 PartOf(c1,c2) | - Enc(c2,f3(c1,c2)). [resolve(73,c,51,a),unit_del(a,49)]. 147 PartOf(c1,c2) | - Enc(c1,f3(c1,c2)). [para(36(a,1),146(b,1)),merge(b)]. 155 PartOf(c1,c2) | Enc(c1,f3(c1,c2)). [resolve(75,c,51,a),unit_del(a,49)]. 156 Enc(c1,f3(c1,c2)) | - Property(x) | - Enc(c1,x) | Enc(c2,x). [resolve(155,a,41,c),unit_del(b,48),unit_del(c,49)]. 177 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | - PartOf(c1,c2) | - PartOf(c2,c1). [resolve(138,c,38,a)]. 185 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | PartOf(c1,c1) | Property(f3(c2,c2)). [para(138(c,1),104(a,2))]. 186 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | PartOf(c1,c1) | Enc(c2,f3(c2,c2)). [para(138(c,1),106(a,2))]. 188 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | PartOf(c1,c1) | Enc(c1,f3(c1,c2)). [para(138(c,1),155(a,2))]. 246 Property(f4(c1,c2)) | c2 = c1. [resolve(79,a,51,a),flip(b)]. 247 Property(f4(c1,c2)) | - PartOf(c1,c2) | - PartOf(c2,c1). [resolve(246,b,38,a)]. 324 Property(f4(c1,c2)) | - PartOf(c1,c1) | - PartOf(c2,c1). [para(246(b,1),247(b,2)),merge(b)]. 334 Property(f4(c1,c2)) | - PartOf(c1,c1). [para(246(b,1),324(c,1)),merge(b),merge(d)]. 335 Property(f4(c1,c2)) | Enc(c1,f3(c1,c1)). [resolve(334,b,99,a)]. 339 Property(f4(c1,c2)) | PartOf(c1,c1). [resolve(335,b,101,b)]. 345 Property(f4(c1,c2)). [resolve(339,b,334,b),merge(b)]. 360 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | - PartOf(c1,c1) | - PartOf(c2,c1). [para(138(c,1),177(c,2)),merge(c),merge(d)]. 389 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | - PartOf(c1,c1). [para(138(c,1),360(d,1)),merge(c),merge(d),merge(f)]. 452 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | Property(f3(c2,c2)). [resolve(185,c,389,c),merge(d),merge(e)]. 455 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | Enc(c2,f3(c2,c2)). [resolve(186,c,389,c),merge(d),merge(e)]. 465 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | Enc(c1,f3(c1,c2)). [resolve(188,c,389,c),merge(d),merge(e)]. 468 PartOf(c2,c1) | Enc(c1,f4(c1,c2)) | Enc(c1,f3(c1,c2)). [para(37(a,1),465(b,1)),merge(c)]. 469 Enc(c1,f4(c1,c2)) | Enc(c1,f3(c1,c2)) | - Property(x) | - Enc(c2,x) | Enc(c1,x). [resolve(468,a,41,c),unit_del(c,49),unit_del(d,48)]. 470 Enc(c1,f4(c1,c2)) | Enc(c1,f3(c1,c2)) | - Enc(c2,f4(c1,c2)). [factor(469,a,e),unit_del(c,345)]. 472 Enc(c1,f4(c1,c2)) | Enc(c1,f3(c1,c2)). [resolve(470,c,465,b),merge(c),merge(d)]. 501 Property(f3(c2,c2)) | Enc(c1,f4(c1,c2)). [resolve(121,c,452,b),merge(d),merge(e),unit_del(b,345)]. 506 Property(f3(c2,c2)) | Enc(c2,f4(c1,c2)). [resolve(501,b,120,c),merge(b),unit_del(b,345)]. 512 Property(f3(c2,c2)) | - Enc(c1,f4(c1,c2)) | c2 = c1. [resolve(506,b,125,b)]. 522 Property(f3(c2,c2)) | c2 = c1. [resolve(512,b,501,b),merge(c)]. 523 Property(f3(c2,c2)) | - PartOf(c1,c2) | - PartOf(c2,c1). [resolve(522,b,38,a)]. 547 Enc(c2,f3(c2,c2)) | Enc(c1,f4(c1,c2)). [resolve(124,c,455,b),merge(d),merge(e),unit_del(b,345)]. 556 Property(f3(c2,c2)) | - PartOf(c1,c2). [resolve(523,c,105,a),merge(c)]. 563 Property(f3(c2,c2)). [resolve(556,b,104,a),merge(b)]. 564 Enc(c2,f3(c2,c2)) | - Enc(c1,f3(c2,c2)). [back_unit_del(123),unit_del(b,563)]. 572 Enc(c1,f4(c1,c2)) | PartOf(c2,c2). [resolve(547,a,100,b)]. 583 PartOf(c1,c2) | Enc(c1,f4(c1,c2)). [para(36(a,1),572(b,1)),merge(c)]. 584 PartOf(c2,c1) | Enc(c1,f4(c1,c2)). [para(37(a,1),572(b,2)),merge(c)]. 587 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)) | PartOf(c1,c1). [para(138(c,1),583(a,2)),merge(d)]. 592 Enc(c1,f4(c1,c2)) | - Property(x) | - Enc(c2,x) | Enc(c1,x). [resolve(584,a,41,c),unit_del(b,49),unit_del(c,48)]. 593 Enc(c1,f4(c1,c2)) | - Enc(c2,f4(c1,c2)). [factor(592,a,d),unit_del(b,345)]. 690 Enc(c1,f3(c1,c2)) | Enc(c2,f4(c1,c2)). [resolve(156,c,472,a),merge(d),unit_del(b,345)]. 702 Enc(c1,f3(c1,c2)) | - Enc(c1,f4(c1,c2)) | c2 = c1. [resolve(690,b,125,b)]. 709 Enc(c1,f4(c1,c2)) | Enc(c2,f4(c1,c2)). [resolve(587,c,389,c),merge(c),merge(d)]. 710 Enc(c1,f4(c1,c2)). [resolve(709,b,593,b),merge(b)]. 711 Enc(c1,f3(c1,c2)) | c2 = c1. [back_unit_del(702),unit_del(b,710)]. 714 - Enc(c2,f4(c1,c2)) | c2 = c1. [back_unit_del(125),unit_del(a,710)]. 716 Enc(c2,f3(c2,c2)) | Enc(c2,f4(c1,c2)). [resolve(710,a,122,c),unit_del(b,345)]. 726 Enc(c1,f3(c1,c2)) | - PartOf(c1,c2) | - PartOf(c2,c1). [resolve(711,b,38,a)]. 736 Enc(c1,f3(c1,c2)) | PartOf(c1,c1). [para(711(b,1),155(a,2)),merge(c)]. 808 Enc(c1,f3(c1,c2)) | PartOf(c2,c1). [resolve(736,b,126,b)]. 812 Enc(c2,f3(c2,c2)) | c2 = c1. [resolve(716,b,714,a)]. 833 Enc(c2,f3(c2,c2)) | - Enc(c1,f3(c1,c2)). [para(812(b,1),564(b,2,1)),merge(b)]. 837 Enc(c1,f3(c1,c2)) | - PartOf(c1,c2). [resolve(726,c,808,b),merge(c)]. 843 Enc(c1,f3(c1,c2)). [resolve(837,b,155,a),merge(b)]. 844 Enc(c2,f3(c2,c2)). [back_unit_del(833),unit_del(b,843)]. 845 PartOf(c1,c2). [back_unit_del(147),unit_del(b,843)]. 847 PartOf(c2,c2). [back_unit_del(100),unit_del(b,844)]. 853 c2 != c1 | - PartOf(c2,c1). [back_unit_del(38),unit_del(b,845)]. 856 PartOf(c2,c1). [para(37(a,1),847(a,2)),merge(b)]. 857 c2 != c1. [back_unit_del(853),unit_del(b,856)]. 860 - Enc(c2,f4(c1,c2)). [back_unit_del(714),unit_del(b,857)]. 864 $F. [ur(41,b,49,a,c,845,a,d,345,a,e,710,a,f,860,a),unit_del(a,48)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=263. Generated=2828. Kept=828. proofs=1. Usable=66. Sos=23. Demods=1. Denials=0. Limbo=0, Disabled=774. Hints=0. Megabytes=0.43. User_CPU=0.10, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3768 exit (max_proofs) Wed Jun 14 17:11:48 2006