============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 48295 was started by zalta on mally.stanford.edu, Fri Nov 4 15:36:21 2016 The command was "mace4 -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all F (Relation1(F) -> ((exists x (Object(x) & Is_the(x,F))) -> (all y (Object(y) -> (Is_the(y,F) -> Ex1(F,y))))))). (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)))))). (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(end_size, 8). % set(print_models_tabular) -> clear(print_models). % From the command line: set(print_models_tabular). ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all F (Relation1(F) -> ((exists x (Object(x) & Is_the(x,F))) -> (all y (Object(y) -> (Is_the(y,F) -> Ex1(F,y))))))) # label(non_clause). [assumption]. 2 (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))) # label(non_clause). [assumption]. 3 (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]. 4 (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) | -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(f1(x)). -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex2(greater_than,f1(x),x). -Object(x) | Ex1(none_greater,x) | -Ex1(conceivable,x) | Ex1(conceivable,f1(x)). -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Object(f2(x)). -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex2(greater_than,f2(x),x). -Object(x) | -Is_the(x,none_greater) | Ex1(e,x) | Ex1(conceivable,f2(x)). Is_the(g,none_greater). end_of_list. ============================== end of clauses for search ============= % There are no natural numbers in the input. ============================== DOMAIN SIZE 2 ========================= conceivable : 0 e : 0 g : 0 greater_than : 0 none_greater : 0 f1 : 0 1 ------- 0 0 f2 : 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. ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=35, kept=35. Selections=21, assignments=21, propagations=8, current_models=1. Rewrite_terms=62, rewrite_bools=71, indexes=40. Rules_from_neg_clauses=0, cross_offs=0. ============================== end of statistics ===================== User_CPU=0.01, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 48295 exit (max_models) Fri Nov 4 15:36:21 2016 The process finished Fri Nov 4 15:36:21 2016