============================== Mace4 ================================= Mace4 (32) version June-2007, June 2007. Process 12212 was started by zalta on mally, Thu Oct 9 16:31:33 2008 The command was "mace -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all F (Relation1(F) -> ((exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))))) -> (exists u (Object(u) & Is_the(u,F)))))). (all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z))))))). (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))). (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). (exists x (Object(x) & Ex1(none_greater,x))). (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y = x))))). (all x (Object(x) -> (Is_the(x,none_greater) & -Ex1(e,x) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))). Is_the(g,none_greater). 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 ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all F (Relation1(F) -> ((exists y (Object(y) & Ex1(F,y) & (all z (Object(z) -> (Ex1(F,z) -> z = y))))) -> (exists u (Object(u) & Is_the(u,F)))))) # label(non_clause). [assumption]. 2 (all F (Relation1(F) -> ((exists y (Object(y) & Is_the(y,F))) -> (all z (Object(z) -> (Is_the(z,F) -> Ex1(F,z))))))) # label(non_clause). [assumption]. 3 (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))) # label(non_clause). [assumption]. 4 (all x (Object(x) -> (Ex1(none_greater,x) <-> Ex1(conceivable,x) & -(exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. 5 (exists x (Object(x) & Ex1(none_greater,x))) # label(non_clause). [assumption]. 6 (exists x (Object(x) & Ex1(none_greater,x))) -> (exists x (Object(x) & Ex1(none_greater,x) & (all y (Object(y) -> (Ex1(none_greater,y) -> y = x))))) # label(non_clause). [assumption]. 7 (all x (Object(x) -> (Is_the(x,none_greater) & -Ex1(e,x) -> (exists y (Object(y) & Ex2(greater_than,y,x) & Ex1(conceivable,y)))))) # label(non_clause). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Object(f2(x)). -Relation1(x) | -Object(y) | -Ex1(x,y) | Object(f1(x,y)) | Is_the(f2(x),x). -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Object(f2(x)). -Relation1(x) | -Object(y) | -Ex1(x,y) | Ex1(x,f1(x,y)) | Is_the(f2(x),x). -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Object(f2(x)). -Relation1(x) | -Object(y) | -Ex1(x,y) | f1(x,y) != y | Is_the(f2(x),x). -Relation1(x) | -Object(y) | -Is_the(y,x) | -Object(z) | -Is_the(z,x) | Ex1(x,z). -Is_the(x,y) | Relation1(y). -Is_the(x,y) | Object(x). -Object(x) | -Ex1(none_greater,x) | Ex1(conceivable,x). -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex2(greater_than,y,x) | -Ex1(conceivable,y). -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Object(f3(x)). -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f3(x),x). -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f3(x)). Object(c1). Ex1(none_greater,c1). -Object(x) | -Ex1(none_greater,x) | Object(c2). -Object(x) | -Ex1(none_greater,x) | Ex1(none_greater,c2). -Object(x) | -Ex1(none_greater,x) | -Object(y) | -Ex1(none_greater,y) | c2 = y. -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f4(x)). -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f4(x),x). -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f4(x)). Is_the(g,none_greater). end_of_list. ============================== end of clauses for search ============= % The maximum domain element in the input is 0. ============================== DOMAIN SIZE 2 ========================= ============================== MODEL ================================= % Model 1 at 0.00 seconds. conceivable : 0 e : 0 g : 0 greater_than : 0 none_greater : 0 c1 : 0 c2 : 0 f2 : 0 1 ------- 0 0 f3 : 0 1 ------- 0 0 f4 : 0 1 ------- 0 0 f1 : | 0 1 --+---- 0 | 0 0 1 | 0 0 Object : 0 1 ------- 1 0 Relation1 : 0 1 ------- 1 0 Ex1 : | 0 1 --+---- 0 | 1 0 1 | 0 0 Is_the : | 0 1 --+---- 0 | 1 0 1 | 0 0 Ex2(0,0,0) = 0. Ex2(0,0,1) = 0. Ex2(0,1,0) = 0. Ex2(0,1,1) = 0. Ex2(1,0,0) = 0. Ex2(1,0,1) = 0. Ex2(1,1,0) = 0. Ex2(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=69, kept=69. Selections=28, assignments=28, propagations=9, current_models=1. Rewrite_terms=133, rewrite_bools=148, indexes=60. 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 12212 exit (max_models) Thu Oct 9 16:31:33 2008 The process finished Thu Oct 9 16:31:33 2008