============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 30283 was started by zalta on mally, Fri Sep 11 16:53:58 2009 The command was "prover9.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 (8 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.01 (+ 0.01) seconds. % Length of proof is 42. % Level of proof is 13. % Maximum clause weight is 14. % Given clauses 37. 1 Object(c1). [clausify]. 5 ActualAt(c1,c2). [clausify]. 13 - Object(x) | - Point(y) | - WorldAt(x,y) | Point(f2(x,y)). [clausify]. 16 - Object(x) | - Proposition(y) | - Point(z) | - TrueInAt(y,x,z) | EncpAt(x,y,z). [clausify]. 17 - Object(x) | - Proposition(y) | - Point(z) | TrueInAt(y,x,z) | - EncpAt(x,y,z). [clausify]. 19 - Object(x) | - Point(y) | - ActualAt(x,y) | - Proposition(z) | - TrueInAt(z,x,y) | True(z,y). [clausify]. 21 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | - Point(u) | EncpAt(x,y,u). [clausify]. 24 - Object(x) | - Point(y) | - WorldAt(x,y) | - Proposition(z) | TrueInAt(z,x,f2(x,y)) | - True(z,f2(x,y)). [clausify]. 35 - Point(x) | - ActualAt(c1,x) | - Proposition(y) | - TrueInAt(y,c1,x) | True(y,x). [resolve(19,a,1,a)]. 44 - Point(c2) | - Proposition(x) | - TrueInAt(x,c1,c2) | True(x,c2). [resolve(35,b,5,a)]. 57 Point(c2). [clausify]. 58 Proposition(c3). [clausify]. 59 WorldAt(c1,c2). [clausify]. 60 TrueInAt(c3,c1,c2) | True(c3,c2). [clausify]. 61 - TrueInAt(c3,c1,c2) | - True(c3,c2). [clausify]. 62 - Point(x) | - Proposition(y) | - True(~ y,x) | - True(y,x). [clausify]. 63 - Proposition(x) | Proposition(~ x). [clausify]. 64 - Point(x) | - Proposition(y) | True(~ y,x) | True(y,x). [clausify]. 65 - Point(x) | - WorldAt(c1,x) | Point(f2(c1,x)). [resolve(13,a,1,a)]. 67 - Proposition(x) | - Point(y) | - TrueInAt(x,c1,y) | EncpAt(c1,x,y). [resolve(16,a,1,a)]. 68 - Proposition(x) | - Point(y) | TrueInAt(x,c1,y) | - EncpAt(c1,x,y). [resolve(17,a,1,a)]. 69 - Proposition(x) | - Point(y) | - EncpAt(c1,x,y) | - Point(z) | EncpAt(c1,x,z). [resolve(21,a,1,a)]. 71 - Point(x) | - WorldAt(c1,x) | - Proposition(y) | TrueInAt(y,c1,f2(c1,x)) | - True(y,f2(c1,x)). [resolve(24,a,1,a)]. 72 - Proposition(x) | - TrueInAt(x,c1,c2) | True(x,c2). [copy(44),unit_del(a,57)]. 76 Proposition(~ c3). [resolve(63,a,58,a)]. 77 - Point(x) | True(~ c3,x) | True(c3,x). [resolve(64,b,58,a)]. 78 Point(f2(c1,c2)). [resolve(65,b,59,a),unit_del(a,57)]. 81 - Proposition(x) | TrueInAt(x,c1,f2(c1,c2)) | - True(x,f2(c1,c2)). [resolve(71,b,59,a),unit_del(a,57)]. 82 True(c3,c2). [resolve(72,b,60,a),merge(c),unit_del(a,58)]. 83 - TrueInAt(c3,c1,c2). [back_unit_del(61),unit_del(b,82)]. 84 - True(~ c3,c2). [ur(62,a,57,a,b,58,a,d,82,a)]. 87 - EncpAt(c1,c3,c2). [ur(68,a,58,a,b,57,a,c,83,a)]. 88 - EncpAt(c1,c3,f2(c1,c2)). [ur(69,a,58,a,b,78,a,d,57,a,e,87,a)]. 90 True(~ c3,f2(c1,c2)) | True(c3,f2(c1,c2)). [resolve(77,a,78,a)]. 91 - TrueInAt(~ c3,c1,c2). [ur(72,a,76,a,c,84,a)]. 92 - TrueInAt(c3,c1,f2(c1,c2)). [ur(67,a,58,a,b,78,a,d,88,a)]. 97 - EncpAt(c1,~ c3,c2). [ur(68,a,76,a,b,57,a,c,91,a)]. 98 - True(c3,f2(c1,c2)). [ur(81,a,58,a,b,92,a)]. 99 True(~ c3,f2(c1,c2)). [back_unit_del(90),unit_del(b,98)]. 100 TrueInAt(~ c3,c1,f2(c1,c2)). [resolve(99,a,81,c),unit_del(a,76)]. 102 EncpAt(c1,~ c3,f2(c1,c2)). [resolve(100,a,67,c),unit_del(a,76),unit_del(b,78)]. 104 $F. [ur(69,a,76,a,b,78,a,d,57,a,e,97,a),unit_del(a,102)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=37. Generated=72. Kept=47. proofs=1. Usable=34. Sos=8. Demods=0. Denials=0. Limbo=0, Disabled=61. Hints=0. Megabytes=0.09. User_CPU=0.01, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 30283 exit (max_proofs) Fri Sep 11 16:53:58 2009