============================== Mace4 ================================= Mace4 (32) version June-2006B, June 2006. Process 30389 was started by zalta on mally, Fri Sep 11 17:12:55 2009 The command was "mace.orig -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). (all x all d (WorldAt(x,d) -> Object(x) & Point(d))). (all x (Object(x) -> ((exists d (Point(d) & WorldAt(x,d))) -> (all d (Point(d) -> WorldAt(x,d)))))). (all x all p (Object(x) & Proposition(p) -> ((exists d (Point(d) & TrueInAt(p,x,d))) -> (all d (Point(d) -> TrueInAt(p,x,d)))))). (all x all d (Object(x) & Point(d) -> (WorldAt(x,d) & ActualAt(x,d) -> (all p (Proposition(p) -> (TrueInAt(p,x,d) <-> True(p,d))))))). (all d (Point(d) -> (exists x (WorldAt(x,d) & ActualAt(x,d))))). Point(W). (all p (NecessarilyTrue(p) <-> (all d (Point(d) -> True(p,d))))). Point(W). (all x (World(x) <-> WorldAt(x,W))). (all x all p (TrueIn(p,x) <-> TrueInAt(p,x,W))). 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. W : 0 f1 : 0 1 ------- 0 0 f2 : 0 1 ------- 0 0 NecessarilyTrue : 0 1 ------- 0 0 Object : 0 1 ------- 1 0 Point : 0 1 ------- 1 0 Proposition : 0 1 ------- 0 0 World : 0 1 ------- 1 0 ActualAt : | 0 1 --+---- 0 | 1 0 1 | 0 0 True : | 0 1 --+---- 0 | 0 0 1 | 0 0 TrueIn : | 0 1 --+---- 0 | 0 0 1 | 0 0 WorldAt : | 0 1 --+---- 0 | 1 0 1 | 0 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.00 seconds). Ground clauses: seen=74, kept=74. Selections=24, assignments=24, propagations=15, current_models=1. Rewrite_terms=22, rewrite_bools=147, indexes=19. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 30389 exit (max_models) Fri Sep 11 17:12:55 2009 The process finished Fri Sep 11 17:12:55 2009