============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3624 was started by root on mally, Wed Jun 14 16:53:55 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 (4 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <90,47>. Problem reduction (0.00 sec) gives one subproblem (<177,45>); reverting to ordinary search with original formulas. ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 15 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.01 (+ 0.02) seconds. % Length of proof is 36. % Level of proof is 8. % Maximum clause weight is 25. % Given clauses 40. 2 IsAFormOf(c2,c1). [clausify]. 3 IsAFormOf(c3,c1). [clausify]. 5 - IsAFormOf(x,y) | Object(x). [clausify]. 7 - Object(x) | - Property(y) | - IsAFormOf(x,y) | Ex1(A,x,W). [clausify]. 8 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | - Enc(x,z) | Implies(y,z). [clausify]. 9 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | Enc(x,z) | - Implies(y,z). [clausify]. 20 - Object(c2) | - Property(c1) | Ex1(A,c2,W). [resolve(7,c,2,a)]. 21 - Object(c3) | - Property(c1) | Ex1(A,c3,W). [resolve(7,c,3,a)]. 22 - Object(c2) | - Property(c1) | - Property(x) | - Enc(c2,x) | Implies(c1,x). [resolve(8,c,2,a)]. 23 - Object(c3) | - Property(c1) | - Property(x) | - Enc(c3,x) | Implies(c1,x). [resolve(8,c,3,a)]. 24 - Object(c2) | - Property(c1) | - Property(x) | Enc(c2,x) | - Implies(c1,x). [resolve(9,c,2,a)]. 25 - Object(c3) | - Property(c1) | - Property(x) | Enc(c3,x) | - Implies(c1,x). [resolve(9,c,3,a)]. 32 Property(c1). [clausify]. 33 c3 != c2. [clausify]. 34 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Property(f2(x,y)) | y = x. [clausify]. 35 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | Enc(x,f2(x,y)) | Enc(y,f2(x,y)) | y = x. [clausify]. 36 - Object(x) | - Object(y) | - Ex1(A,x,W) | - Ex1(A,y,W) | - Enc(x,f2(x,y)) | - Enc(y,f2(x,y)) | y = x. [clausify]. 37 Object(c2). [resolve(5,a,2,a)]. 38 Object(c3). [resolve(5,a,3,a)]. 39 Ex1(A,c2,W). [copy(20),unit_del(a,37),unit_del(b,32)]. 40 Ex1(A,c3,W). [copy(21),unit_del(a,38),unit_del(b,32)]. 41 - Property(x) | - Enc(c2,x) | Implies(c1,x). [copy(22),unit_del(a,37),unit_del(b,32)]. 42 - Property(x) | - Enc(c3,x) | Implies(c1,x). [copy(23),unit_del(a,38),unit_del(b,32)]. 43 - Property(x) | Enc(c2,x) | - Implies(c1,x). [copy(24),unit_del(a,37),unit_del(b,32)]. 44 - Property(x) | Enc(c3,x) | - Implies(c1,x). [copy(25),unit_del(a,38),unit_del(b,32)]. 57 - Object(x) | - Ex1(A,x,W) | - Enc(x,f2(x,c2)) | - Enc(c2,f2(x,c2)) | c2 = x. [resolve(39,a,36,d),unit_del(b,37)]. 59 - Object(x) | - Ex1(A,x,W) | Enc(x,f2(x,c2)) | Enc(c2,f2(x,c2)) | c2 = x. [resolve(39,a,35,d),unit_del(b,37)]. 61 - Object(x) | - Ex1(A,x,W) | Property(f2(x,c2)) | c2 = x. [resolve(39,a,34,d),unit_del(b,37)]. 93 - Enc(c3,f2(c3,c2)) | - Enc(c2,f2(c3,c2)). [resolve(57,b,40,a),flip(d),unit_del(a,38),unit_del(d,33)]. 95 Property(f2(c3,c2)). [resolve(61,b,40,a),flip(c),unit_del(a,38),unit_del(c,33)]. 96 Enc(c3,f2(c3,c2)) | Enc(c2,f2(c3,c2)). [resolve(59,b,40,a),flip(d),unit_del(a,38),unit_del(d,33)]. 98 Enc(c2,f2(c3,c2)) | Implies(c1,f2(c3,c2)). [resolve(96,a,42,b),unit_del(b,95)]. 99 Enc(c2,f2(c3,c2)). [resolve(98,b,43,c),merge(c),unit_del(b,95)]. 100 - Enc(c3,f2(c3,c2)). [back_unit_del(93),unit_del(b,99)]. 102 Implies(c1,f2(c3,c2)). [resolve(99,a,41,b),unit_del(a,95)]. 103 $F. [resolve(102,a,44,c),unit_del(a,95),unit_del(b,100)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=40. Generated=121. Kept=71. proofs=1. Usable=37. Sos=30. Demods=0. Denials=0. Limbo=0, Disabled=34. Hints=0. Megabytes=0.12. User_CPU=0.01, System_CPU=0.02, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3624 exit (max_proofs) Wed Jun 14 16:53:55 2006