============================== Mace4 ================================= Mace4 (32) version June-2006B, June 2006. Process 3793 was started by zalta on mally, Wed Jun 14 17:16:13 2006 The command was "mace -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= op(300,prefix,~). formulas(sos). (all p (Proposition(p) -> Proposition(~ p))). (all d all p (Point(d) & Proposition(p) -> (True(~ p,d) <-> - True(p,d)))). (all x (Situation(x) -> Object(x))). (all x (Object(x) -> (Possible(x) <-> Situation(x) & (exists y (Point(y) & (all p (Proposition(p) -> (TrueIn(p,x) -> True(p,y))))))))). (all x (Object(x) -> (Consistent(x) <-> Situation(x) & - (exists p (Proposition(p) & TrueIn(p,x) & TrueIn(~ p,x)))))). 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. ~ : 0 1 ------- 0 0 f1 : 0 1 ------- 0 0 f3 : 0 1 ------- 0 0 f2 : | 0 1 --+---- 0 | 0 0 1 | 0 0 Consistent : 0 1 ------- 0 0 Object : 0 1 ------- 0 0 Point : 0 1 ------- 0 0 Possible : 0 1 ------- 0 0 Proposition : 0 1 ------- 0 0 Situation : 0 1 ------- 0 0 True : | 0 1 --+---- 0 | 0 0 1 | 0 0 TrueIn : | 0 1 --+---- 0 | 0 0 1 | 0 0 ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=44, kept=44. Selections=27, assignments=27, propagations=3, current_models=1. Rewrite_terms=40, rewrite_bools=57, indexes=26. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 3793 exit (max_models) Wed Jun 14 17:16:13 2006 The process finished Wed Jun 14 17:16:13 2006