============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 14081 was started by zalta on mally, Sat Jul 21 18:42:23 2007 The command was "prove.orig". ============================== 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 (7 formulas) ============================== end of input ========================== ============================== PROCESS INITIAL CLAUSES =============== % Assigned IDs to 26 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.00) seconds. % Length of proof is 31. % Level of proof is 7. % Maximum clause weight is 9. % Given clauses 22. 1 Point(W). [clausify]. 2 Object(c1). [clausify]. 5 Property(c2). [clausify]. 14 - Object(x) | - Proposition(y) | TrueIn(y,x) | - Encp(x,y). [clausify]. 18 - Object(x) | - Actual(x) | - Proposition(y) | - TrueIn(y,x) | True(y,W). [clausify]. 20 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f1(x,y)). [clausify]. 23 - Object(x) | - Proposition(y) | - Point(z) | Ex1At(VAC(y),x,z) | - True(y,z). [clausify]. 24 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f1(x,y)) = y. [clausify]. 26 - Object(x) | - Proposition(y) | Encp(x,y) | - Property(z) | VAC(y) != z | - Enc(x,z). [clausify]. 28 - Object(x) | - Proposition(y) | Ex1At(VAC(y),x,W) | - True(y,W). [resolve(23,c,1,a)]. 39 - Actual(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,W). [resolve(18,a,2,a)]. 41 - Situation(c1) | - Property(x) | - Enc(c1,x) | Proposition(f1(c1,x)). [resolve(20,a,2,a)]. 43 - Situation(c1) | - Property(x) | - Enc(c1,x) | VAC(f1(c1,x)) = x. [resolve(24,a,2,a)]. 45 - Proposition(x) | Encp(c1,x) | - Property(y) | VAC(x) != y | - Enc(c1,y). [resolve(26,a,2,a)]. 48 - Situation(c1) | - Enc(c1,c2) | Proposition(f1(c1,c2)). [resolve(41,b,5,a)]. 50 - Situation(c1) | - Enc(c1,c2) | VAC(f1(c1,c2)) = c2. [resolve(43,b,5,a)]. 52 - Proposition(x) | Encp(c1,x) | VAC(x) != c2 | - Enc(c1,c2). [resolve(45,c,5,a)]. 55 Situation(c1). [clausify]. 56 Actual(c1). [clausify]. 57 Enc(c1,c2). [clausify]. 58 - Ex1At(c2,c1,W). [clausify]. 61 - Proposition(x) | TrueIn(x,c1) | - Encp(c1,x). [resolve(14,a,2,a)]. 62 - Proposition(x) | - TrueIn(x,c1) | True(x,W). [copy(39),unit_del(a,56)]. 66 - Proposition(x) | Ex1At(VAC(x),c1,W) | - True(x,W). [resolve(28,a,2,a)]. 67 Proposition(f1(c1,c2)). [copy(48),unit_del(a,55),unit_del(b,57)]. 69 VAC(f1(c1,c2)) = c2. [copy(50),unit_del(a,55),unit_del(b,57)]. 71 - Proposition(x) | Encp(c1,x) | VAC(x) != c2. [copy(52),unit_del(d,57)]. 73 Encp(c1,f1(c1,c2)). [resolve(71,c,69,a),unit_del(a,67)]. 77 TrueIn(f1(c1,c2),c1). [resolve(73,a,61,c),unit_del(a,67)]. 78 True(f1(c1,c2),W). [resolve(77,a,62,b),unit_del(a,67)]. 79 $F. [resolve(78,a,66,c),demod(69(8)),unit_del(a,67),unit_del(b,58)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=22. Generated=46. Kept=24. proofs=1. Usable=22. Sos=0. Demods=2. Denials=0. Limbo=0, Disabled=56. Hints=0. Megabytes=0.07. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 14081 exit (max_proofs) Sat Jul 21 18:42:23 2007