============================== Mace4 ================================= Mace4 (32) version June-2006B, June 2006. Process 3695 was started by zalta on mally, Wed Jun 14 17:02:14 2006 The command was "mace -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= set(auto2). WARNING, flag not recognized: set(auto2). formulas(sos). Property(A). (all F all G (Property(F) & Property(G) -> (Implies(F,G) <-> (all x all w (Point(w) -> (Ex1(F,x,w) -> Ex1(G,x,w))))))). (all x all G (Object(x) & Property(G) -> (IsAFormOf(x,G) <-> Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))). (all x all G (IsAFormOf(x,G) -> Object(x) & Property(G))). (all x all y (Object(x) & Object(y) -> (PartPH(x,y) <-> (exists F (Property(F) & IsTheFormOf(y,F) & Enc(x,F)))))). (all x all G (Object(x) & Property(G) -> (IsTheFormOf(x,G) <-> IsAFormOf(x,G) & (all y (IsAFormOf(y,G) -> y = x))))). (all G (Property(G) -> (exists x (Object(x) & Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F)))))))). (all x all y (Object(x) & Object(y) & Ex1(A,x,W) & Ex1(A,y,W) -> ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) -> x = y))). 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 W : 0 f6 : 0 1 ------- 0 0 f1 : | 0 1 --+---- 0 | 0 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 f5 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f7 : | 0 1 --+---- 0 | 0 0 1 | 0 0 Object : 0 1 ------- 1 0 Point : 0 1 ------- 0 0 Property : 0 1 ------- 1 0 Enc : | 0 1 --+---- 0 | 1 0 1 | 0 0 Implies : | 0 1 --+---- 0 | 1 0 1 | 0 0 IsAFormOf : | 0 1 --+---- 0 | 1 0 1 | 0 0 IsTheFormOf : | 0 1 --+---- 0 | 1 0 1 | 0 0 PartPH : | 0 1 --+---- 0 | 1 0 1 | 0 0 Ex1(0,0,0) = 1. Ex1(0,0,1) = 0. Ex1(0,1,0) = 0. Ex1(0,1,1) = 0. Ex1(1,0,0) = 0. Ex1(1,0,1) = 0. Ex1(1,1,0) = 0. Ex1(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=133, kept=123. Selections=51, assignments=51, propagations=11, current_models=1. Rewrite_terms=143, rewrite_bools=279, indexes=61. 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 3695 exit (max_models) Wed Jun 14 17:02:14 2006 The process finished Wed Jun 14 17:02:14 2006