============================== Mace4 ================================= Mace4 (32) version June-2006B, June 2006. Process 30317 was started by zalta on mally, Fri Sep 11 16:57:31 2009 The command was "mace.orig -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). (all p all q (Proposition(p) & Proposition(q) -> (VAC(p) = VAC(q) -> p = q))). (all p (Proposition(p) <-> Property(VAC(p)))). (all x all d (Object(x) & Point(d) -> (SituationAt(x,d) <-> Ex1At(A,x,d) & (all F (Property(F) -> (EncAt(x,F,d) -> (exists p (Proposition(p) & F = VAC(p))))))))). (all x all d (Object(x) & Point(d) -> (ActualAt(x,d) <-> SituationAt(x,d) & (all p (Proposition(p) -> (TrueInAt(p,x,d) -> True(p,d))))))). (all x all d (Object(x) & Point(d) -> (WorldAt(x,d) <-> SituationAt(x,d) & (exists d2 (Point(d2) & (all p (Proposition(p) -> (TrueInAt(p,x,d2) <-> True(p,d2))))))))). (all x all p all d (Object(x) & Proposition(p) & Point(d) -> (EncpAt(x,p,d) <-> (exists F (Property(F) & F = VAC(p) & EncAt(x,F,d)))))). (all p all x all d (Object(x) & Proposition(p) & Point(d) -> (TrueInAt(p,x,d) <-> EncpAt(x,p,d)))). (all d (Point(d) -> (exists x (Object(x) & Ex1At(A,x,d) & (all F (Property(F) -> (EncAt(x,F,d) <-> (exists p (Proposition(p) & True(p,d) & F = VAC(p)))))))))). end_of_list. % From the command line: assign(iterate_up_to, 8). % set(print_models) -> clear(print_models_portable). % From the command line: set(print_models). ============================== end of input ========================== % The maximum domain element in the input is 0. ============================== DOMAIN SIZE 2 ========================= ============================== MODEL ================================= % Model 1 at 0.00 seconds. A : 0 VAC : 0 1 ------- 0 0 f7 : 0 1 ------- 0 0 f2 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f3 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f4 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f8 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f1(0,0,0) = 0. f1(0,0,1) = 0. f1(0,1,0) = 0. f1(0,1,1) = 0. f1(1,0,0) = 0. f1(1,0,1) = 0. f1(1,1,0) = 0. f1(1,1,1) = 0. f5(0,0,0) = 0. f5(0,0,1) = 0. f5(0,1,0) = 0. f5(0,1,1) = 0. f5(1,0,0) = 0. f5(1,0,1) = 0. f5(1,1,0) = 0. f5(1,1,1) = 0. f6(0,0,0) = 0. f6(0,0,1) = 0. f6(0,1,0) = 0. f6(0,1,1) = 0. f6(1,0,0) = 0. f6(1,0,1) = 0. f6(1,1,0) = 0. f6(1,1,1) = 0. Object : 0 1 ------- 0 0 Point : 0 1 ------- 0 0 Property : 0 1 ------- 0 0 Proposition : 0 1 ------- 0 0 ActualAt : | 0 1 --+---- 0 | 0 0 1 | 0 0 SituationAt : | 0 1 --+---- 0 | 0 0 1 | 0 0 True : | 0 1 --+---- 0 | 0 0 1 | 0 0 WorldAt : | 0 1 --+---- 0 | 0 0 1 | 0 0 EncAt(0,0,0) = 0. EncAt(0,0,1) = 0. EncAt(0,1,0) = 0. EncAt(0,1,1) = 0. EncAt(1,0,0) = 0. EncAt(1,0,1) = 0. EncAt(1,1,0) = 0. EncAt(1,1,1) = 0. EncpAt(0,0,0) = 0. EncpAt(0,0,1) = 0. EncpAt(0,1,0) = 0. EncpAt(0,1,1) = 0. EncpAt(1,0,0) = 0. EncpAt(1,0,1) = 0. EncpAt(1,1,0) = 0. EncpAt(1,1,1) = 0. Ex1At(0,0,0) = 0. Ex1At(0,0,1) = 0. Ex1At(0,1,0) = 0. Ex1At(0,1,1) = 0. Ex1At(1,0,0) = 0. Ex1At(1,0,1) = 0. Ex1At(1,1,0) = 0. Ex1At(1,1,1) = 0. TrueInAt(0,0,0) = 0. TrueInAt(0,0,1) = 0. TrueInAt(0,1,0) = 0. TrueInAt(0,1,1) = 0. TrueInAt(1,0,0) = 0. TrueInAt(1,0,1) = 0. TrueInAt(1,1,0) = 0. TrueInAt(1,1,1) = 0. ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=196, kept=194. Selections=97, assignments=97, propagations=4, current_models=1. Rewrite_terms=262, rewrite_bools=205, indexes=121. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== User_CPU=0.01, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 30317 exit (max_models) Fri Sep 11 16:57:31 2009 The process finished Fri Sep 11 16:57:31 2009