============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 30334 was started by zalta on mally, Fri Sep 11 16:58:36 2009 The command was "prover9.orig". ============================== 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 (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.01 seconds. ============================== PROOF ================================= % Proof 1 at 0.06 (+ 0.01) seconds. % Length of proof is 66. % Level of proof is 25. % Maximum clause weight is 24. % Given clauses 157. 1 Object(c1). [clausify]. 6 - Object(x) | - Point(y) | - WorldAt(x,y) | SituationAt(x,y). [clausify]. 7 - Object(x) | - Point(y) | - WorldAt(x,y) | Point(f1(x,y)). [clausify]. 8 - Object(x) | - Point(y) | - SituationAt(x,y) | Ex1At(A,x,y). [clausify]. 9 - Object(x) | - Point(y) | - Ex1At(A,x,y) | - Point(z) | Ex1At(A,x,z). [clausify]. 12 - Object(x) | - Point(y) | SituationAt(x,y) | - Ex1At(A,x,y) | Property(f4(x,y)). [clausify]. 14 - Object(x) | - Property(y) | - Point(z) | - EncAt(x,y,z) | - Point(u) | EncAt(x,y,u). [clausify]. 15 - Object(x) | - Point(y) | WorldAt(x,y) | - SituationAt(x,y) | - Point(z) | Proposition(f2(x,y,z)). [clausify]. 16 - Object(x) | - Point(y) | SituationAt(x,y) | - Ex1At(A,x,y) | EncAt(x,f4(x,y),y). [clausify]. 19 - Object(x) | - Point(y) | - SituationAt(x,y) | - Property(z) | - EncAt(x,z,y) | Proposition(f3(x,y,z)). [clausify]. 20 - Object(x) | - Point(y) | SituationAt(x,y) | - Ex1At(A,x,y) | - Proposition(z) | VAC(z) != f4(x,y). [clausify]. 21 - Object(x) | - Point(y) | - WorldAt(x,y) | - Proposition(z) | - TrueInAt(z,x,f1(x,y)) | True(z,f1(x,y)). [clausify]. 22 - Object(x) | - Point(y) | - WorldAt(x,y) | - Proposition(z) | TrueInAt(z,x,f1(x,y)) | - True(z,f1(x,y)). [clausify]. 23 - Object(x) | - Point(y) | - SituationAt(x,y) | - Property(z) | - EncAt(x,z,y) | VAC(f3(x,y,z)) = z. [clausify]. 25 - Object(x) | - Point(y) | WorldAt(x,y) | - SituationAt(x,y) | - Point(z) | TrueInAt(f2(x,y,z),x,z) | True(f2(x,y,z),z). [clausify]. 26 - Object(x) | - Point(y) | WorldAt(x,y) | - SituationAt(x,y) | - Point(z) | - TrueInAt(f2(x,y,z),x,z) | - True(f2(x,y,z),z). [clausify]. 36 - Point(x) | WorldAt(c1,x) | - SituationAt(c1,x) | - Point(y) | Proposition(f2(c1,x,y)). [resolve(15,a,1,a)]. 40 - Point(x) | - SituationAt(c1,x) | - Property(y) | - EncAt(c1,y,x) | Proposition(f3(c1,x,y)). [resolve(19,a,1,a)]. 41 - Point(x) | SituationAt(c1,x) | - Ex1At(A,c1,x) | - Proposition(y) | VAC(y) != f4(c1,x). [resolve(20,a,1,a)]. 42 - Point(x) | - WorldAt(c1,x) | - Proposition(y) | - TrueInAt(y,c1,f1(c1,x)) | True(y,f1(c1,x)). [resolve(21,a,1,a)]. 43 - Point(x) | - WorldAt(c1,x) | - Proposition(y) | TrueInAt(y,c1,f1(c1,x)) | - True(y,f1(c1,x)). [resolve(22,a,1,a)]. 59 - Point(x) | SituationAt(c1,x) | - Ex1At(A,c1,x) | VAC(f3(c1,y,z)) != f4(c1,x) | - Point(y) | - SituationAt(c1,y) | - Property(z) | - EncAt(c1,z,y). [resolve(41,d,40,e)]. 66 Point(c2). [clausify]. 67 Point(c3). [clausify]. 68 WorldAt(c1,c2). [clausify]. 69 - WorldAt(c1,c3). [clausify]. 70 - Point(x) | - WorldAt(c1,x) | SituationAt(c1,x). [resolve(6,a,1,a)]. 71 - Point(x) | - WorldAt(c1,x) | Point(f1(c1,x)). [resolve(7,a,1,a)]. 72 - Point(x) | - SituationAt(c1,x) | Ex1At(A,c1,x). [resolve(8,a,1,a)]. 73 - Point(x) | - Ex1At(A,c1,x) | - Point(y) | Ex1At(A,c1,y). [resolve(9,a,1,a)]. 74 - Point(x) | SituationAt(c1,x) | - Ex1At(A,c1,x) | Property(f4(c1,x)). [resolve(12,a,1,a)]. 75 - Property(x) | - Point(y) | - EncAt(c1,x,y) | - Point(z) | EncAt(c1,x,z). [resolve(14,a,1,a)]. 76 - Point(x) | SituationAt(c1,x) | - Ex1At(A,c1,x) | EncAt(c1,f4(c1,x),x). [resolve(16,a,1,a)]. 77 - Point(x) | - SituationAt(c1,x) | - Property(y) | - EncAt(c1,y,x) | VAC(f3(c1,x,y)) = y. [resolve(23,a,1,a)]. 78 - Point(x) | WorldAt(c1,x) | - SituationAt(c1,x) | - Point(y) | TrueInAt(f2(c1,x,y),c1,y) | True(f2(c1,x,y),y). [resolve(25,a,1,a)]. 79 - Point(x) | WorldAt(c1,x) | - SituationAt(c1,x) | - Point(y) | - TrueInAt(f2(c1,x,y),c1,y) | - True(f2(c1,x,y),y). [resolve(26,a,1,a)]. 91 - Point(x) | SituationAt(c1,x) | - Ex1At(A,c1,x) | f4(c1,x) != VAC(f3(c1,y,z)) | - Point(y) | - SituationAt(c1,y) | - Property(z) | - EncAt(c1,z,y). [copy(59),flip(d)]. 92 - Point(x) | - WorldAt(c1,x) | - TrueInAt(f2(c1,y,z),c1,f1(c1,x)) | True(f2(c1,y,z),f1(c1,x)) | - Point(y) | WorldAt(c1,y) | - SituationAt(c1,y) | - Point(z). [resolve(42,c,36,e)]. 94 - Point(x) | - WorldAt(c1,x) | TrueInAt(f2(c1,y,z),c1,f1(c1,x)) | - True(f2(c1,y,z),f1(c1,x)) | - Point(y) | WorldAt(c1,y) | - SituationAt(c1,y) | - Point(z). [resolve(43,c,36,e)]. 140 SituationAt(c1,c2). [resolve(70,b,68,a),unit_del(a,66)]. 141 Point(f1(c1,c2)). [resolve(71,b,68,a),unit_del(a,66)]. 149 Ex1At(A,c1,c2). [resolve(140,a,72,b),unit_del(a,66)]. 150 - Point(x) | Ex1At(A,c1,x). [resolve(149,a,73,b),unit_del(a,66)]. 152 Ex1At(A,c1,c3). [resolve(150,a,67,a)]. 153 SituationAt(c1,c3) | EncAt(c1,f4(c1,c3),c3). [resolve(152,a,76,c),unit_del(a,67)]. 154 SituationAt(c1,c3) | Property(f4(c1,c3)). [resolve(152,a,74,c),unit_del(a,67)]. 157 SituationAt(c1,c3) | - Property(f4(c1,c3)) | - Point(x) | EncAt(c1,f4(c1,c3),x). [resolve(153,b,75,c),unit_del(c,67)]. 159 Property(f4(c1,c3)) | - Point(x) | TrueInAt(f2(c1,c3,x),c1,x) | True(f2(c1,c3,x),x). [resolve(154,a,78,c),unit_del(b,67),unit_del(c,69)]. 173 Property(f4(c1,c3)) | TrueInAt(f2(c1,c3,f1(c1,c2)),c1,f1(c1,c2)) | True(f2(c1,c3,f1(c1,c2)),f1(c1,c2)). [resolve(159,b,141,a)]. 203 Property(f4(c1,c3)) | True(f2(c1,c3,f1(c1,c2)),f1(c1,c2)) | - SituationAt(c1,c3). [resolve(173,b,92,c),merge(e),unit_del(c,66),unit_del(d,68),unit_del(e,67),unit_del(f,69),unit_del(h,141)]. 204 Property(f4(c1,c3)) | True(f2(c1,c3,f1(c1,c2)),f1(c1,c2)). [resolve(203,c,154,a),merge(c)]. 205 Property(f4(c1,c3)) | TrueInAt(f2(c1,c3,f1(c1,c2)),c1,f1(c1,c2)) | - SituationAt(c1,c3). [resolve(204,b,94,d),unit_del(b,66),unit_del(c,68),unit_del(e,67),unit_del(f,69),unit_del(h,141)]. 206 Property(f4(c1,c3)) | TrueInAt(f2(c1,c3,f1(c1,c2)),c1,f1(c1,c2)). [resolve(205,c,154,a),merge(c)]. 210 Property(f4(c1,c3)) | - SituationAt(c1,c3) | - True(f2(c1,c3,f1(c1,c2)),f1(c1,c2)). [resolve(206,b,79,e),unit_del(b,67),unit_del(c,69),unit_del(e,141)]. 215 Property(f4(c1,c3)) | - SituationAt(c1,c3). [resolve(210,c,204,b),merge(c)]. 216 Property(f4(c1,c3)). [resolve(215,b,154,a),merge(b)]. 217 SituationAt(c1,c3) | - Point(x) | EncAt(c1,f4(c1,c3),x). [back_unit_del(157),unit_del(b,216)]. 219 SituationAt(c1,c3) | EncAt(c1,f4(c1,c3),c2). [resolve(217,b,66,a)]. 222 SituationAt(c1,c3) | VAC(f3(c1,c2,f4(c1,c3))) = f4(c1,c3). [resolve(219,b,77,d),unit_del(b,66),unit_del(c,140),unit_del(d,216)]. 229 SituationAt(c1,c3) | - EncAt(c1,f4(c1,c3),c2). [resolve(222,b,91,d(flip)),merge(c),unit_del(b,67),unit_del(c,152),unit_del(d,66),unit_del(e,140),unit_del(f,216)]. 230 SituationAt(c1,c3). [resolve(229,b,219,b),merge(b)]. 232 - Point(x) | TrueInAt(f2(c1,c3,x),c1,x) | True(f2(c1,c3,x),x). [resolve(230,a,78,c),unit_del(a,67),unit_del(b,69)]. 247 TrueInAt(f2(c1,c3,f1(c1,c2)),c1,f1(c1,c2)) | True(f2(c1,c3,f1(c1,c2)),f1(c1,c2)). [resolve(232,a,141,a)]. 267 True(f2(c1,c3,f1(c1,c2)),f1(c1,c2)). [resolve(247,a,92,c),merge(d),unit_del(b,66),unit_del(c,68),unit_del(d,67),unit_del(e,69),unit_del(f,230),unit_del(g,141)]. 270 TrueInAt(f2(c1,c3,f1(c1,c2)),c1,f1(c1,c2)). [resolve(267,a,94,d),unit_del(a,66),unit_del(b,68),unit_del(d,67),unit_del(e,69),unit_del(f,230),unit_del(g,141)]. 271 $F. [ur(79,a,67,a,b,69,a,c,230,a,d,141,a,f,267,a),unit_del(a,270)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=157. Generated=386. Kept=205. proofs=1. Usable=111. Sos=19. Demods=0. Denials=0. Limbo=1, Disabled=139. Hints=0. Megabytes=0.33. User_CPU=0.06, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 30334 exit (max_proofs) Fri Sep 11 16:58:36 2009