============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3758 was started by zalta on mally, Wed Jun 14 17:10:04 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 (9 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 19 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.00 (+ 0.01) seconds. % Length of proof is 41. % Level of proof is 11. % Maximum clause weight is 16. % Given clauses 35. 1 Point(W). [clausify]. 2 World(ALPHA). [clausify]. 7 - World(x) | Object(x). [clausify]. 11 Object(x) | - Proposition(PLUG(y,x)). [clausify]. 13 - Property(x) | - Object(y) | Proposition(PLUG(x,y)). [clausify]. 16 - Object(x) | - Proposition(y) | - Point(z) | - Ex1At(VAC(y),x,z) | True(y,z). [clausify]. 17 - Object(x) | - Proposition(y) | - Point(z) | Ex1At(VAC(y),x,z) | - True(y,z). [clausify]. 18 - Object(x) | - Property(y) | - Point(z) | - True(PLUG(y,x),z) | Ex1At(y,x,z). [clausify]. 19 - Object(x) | - Property(y) | - Point(z) | True(PLUG(y,x),z) | - Ex1At(y,x,z). [clausify]. 20 - Object(x) | - Proposition(y) | - Ex1At(VAC(y),x,W) | True(y,W). [resolve(16,c,1,a)]. 21 - Object(x) | - Proposition(y) | Ex1At(VAC(y),x,W) | - True(y,W). [resolve(17,c,1,a)]. 22 - Object(x) | - Property(y) | - True(PLUG(y,x),W) | Ex1At(y,x,W). [resolve(18,c,1,a)]. 23 - Object(x) | - Property(y) | True(PLUG(y,x),W) | - Ex1At(y,x,W). [resolve(19,c,1,a)]. 24 Object(ALPHA). [resolve(7,a,2,a)]. 37 Proposition(c1). [clausify]. 38 True(c1,W) | TrueIn(PLUG(VAC(c1),ALPHA),ALPHA). [clausify]. 39 - True(c1,W) | - TrueIn(PLUG(VAC(c1),ALPHA),ALPHA). [clausify]. 40 - Proposition(x) | Property(VAC(x)). [clausify]. 43 - Proposition(x) | - TrueIn(x,ALPHA) | Ex1At(VAC(x),ALPHA,W). [clausify]. 44 - Proposition(x) | TrueIn(x,ALPHA) | - Ex1At(VAC(x),ALPHA,W). [clausify]. 46 - Proposition(x) | - Ex1At(VAC(x),y,W) | True(x,W) | - Proposition(PLUG(z,y)). [resolve(20,a,11,a)]. 47 - Proposition(x) | Ex1At(VAC(x),y,W) | - True(x,W) | - Proposition(PLUG(z,y)). [resolve(21,a,11,a)]. 50 - Property(x) | Proposition(PLUG(x,ALPHA)). [resolve(24,a,13,b)]. 51 - Proposition(x) | - Ex1At(VAC(x),ALPHA,W) | True(x,W). [resolve(24,a,20,a)]. 52 - Proposition(x) | Ex1At(VAC(x),ALPHA,W) | - True(x,W). [resolve(24,a,21,a)]. 53 - Property(x) | - True(PLUG(x,ALPHA),W) | Ex1At(x,ALPHA,W). [resolve(24,a,22,a)]. 54 - Property(x) | True(PLUG(x,ALPHA),W) | - Ex1At(x,ALPHA,W). [resolve(24,a,23,a)]. 55 - Proposition(PLUG(x,y)) | - Ex1At(VAC(PLUG(x,y)),y,W) | True(PLUG(x,y),W). [factor(46,a,d)]. 56 - Proposition(PLUG(x,y)) | Ex1At(VAC(PLUG(x,y)),y,W) | - True(PLUG(x,y),W). [factor(47,a,d)]. 57 Property(VAC(c1)). [resolve(40,a,37,a)]. 58 - Proposition(PLUG(VAC(c1),ALPHA)) | Ex1At(VAC(PLUG(VAC(c1),ALPHA)),ALPHA,W) | True(c1,W). [resolve(43,b,38,b)]. 59 Proposition(PLUG(VAC(c1),ALPHA)). [resolve(57,a,50,a)]. 61 Ex1At(VAC(PLUG(VAC(c1),ALPHA)),ALPHA,W) | True(c1,W). [back_unit_del(58),unit_del(a,59)]. 68 True(c1,W) | True(PLUG(VAC(c1),ALPHA),W). [resolve(61,a,55,b),unit_del(b,59)]. 70 True(c1,W) | Ex1At(VAC(c1),ALPHA,W). [resolve(68,b,53,b),unit_del(b,57)]. 72 True(c1,W). [resolve(70,b,51,b),merge(c),unit_del(b,37)]. 73 - TrueIn(PLUG(VAC(c1),ALPHA),ALPHA). [back_unit_del(39),unit_del(a,72)]. 74 - Ex1At(VAC(PLUG(VAC(c1),ALPHA)),ALPHA,W). [ur(44,a,59,a,b,73,a)]. 75 - True(PLUG(VAC(c1),ALPHA),W). [ur(56,a,59,a,b,74,a)]. 77 Ex1At(VAC(c1),ALPHA,W). [resolve(72,a,52,c),unit_del(a,37)]. 79 $F. [resolve(77,a,54,c),unit_del(a,57),unit_del(b,75)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=35. Generated=72. Kept=43. proofs=1. Usable=30. Sos=5. Demods=0. Denials=0. Limbo=0, Disabled=43. Hints=0. Megabytes=0.07. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3758 exit (max_proofs) Wed Jun 14 17:10:04 2006