============================== Mace4 ================================= Mace4 (32) version June-2006B, June 2006. Process 13574 was started by zalta on mally, Sat Jul 21 16:08:04 2007 The command was "mace.orig -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). Point(W). True(T,W). Proposition(L). - True(L,W). (all p (Proposition(p) <-> Property(VAC(p)))). (all x all p (Object(x) & Proposition(p) -> (Encp(x,p) <-> (exists F (Property(F) & F = VAC(p) & Enc(x,F)))))). (all p all d all x (Object(x) & Proposition(p) & Point(d) -> (Ex1At(VAC(p),x,d) <-> True(p,d)))). (all x (Object(x) -> (Situation(x) <-> Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) -> (exists p (Proposition(p) & F = VAC(p))))))))). (all p all x (Object(x) & Proposition(p) -> (TrueIn(p,x) <-> Encp(x,p)))). (all x (Object(x) -> (Actual(x) <-> Situation(x) & (all p (Proposition(p) -> (TrueIn(p,x) -> True(p,W))))))). (exists x (Object(x) & Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> F = VAC(T)))))). (exists x (Object(x) & Ex1At(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> F = VAC(L)))))). 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 L : 0 T : 1 W : 0 c1 : 0 c2 : 1 VAC : 0 1 ------- 1 0 f3 : 0 1 ------- 0 0 f4 : 0 1 ------- 0 0 f1 : | 0 1 --+---- 0 | 0 0 1 | 1 0 f2 : | 0 1 --+---- 0 | 0 0 1 | 0 0 Actual : 0 1 ------- 1 0 Object : 0 1 ------- 1 1 Point : 0 1 ------- 1 0 Property : 0 1 ------- 0 1 Proposition : 0 1 ------- 1 0 Situation : 0 1 ------- 1 1 Enc : | 0 1 --+---- 0 | 0 0 1 | 0 1 Encp : | 0 1 --+---- 0 | 0 0 1 | 1 0 True : | 0 1 --+---- 0 | 0 0 1 | 1 0 TrueIn : | 0 1 --+---- 0 | 0 1 1 | 0 0 Ex1At(0,0,0) = 1. Ex1At(0,0,1) = 0. Ex1At(0,1,0) = 1. 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. ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=94, kept=94. Selections=31, assignments=35, propagations=39, current_models=1. Rewrite_terms=213, rewrite_bools=301, indexes=103. Rules_from_neg_clauses=4, cross_offs=4. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 13574 exit (max_models) Sat Jul 21 16:08:04 2007 The process finished Sat Jul 21 16:08:04 2007