============================== Mace4 ================================= Mace4 (32) version June-2007, June 2007. Process 20589 was started by zalta on mally, Fri Jul 27 15:11:40 2007 The command was "mace -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(assumptions). (all x (object(x) -> -relation1(x))). (all x (object(x) -> -relation2(x))). (all F (relation1(F) -> -relation2(F))). (all x all F (exemplifies1(F,x) -> relation1(F) & object(x))). (all x all y all R (exemplifies2(R,x,y) -> relation2(R) & object(x) & object(y))). (all x all F (is_the(x,F) -> relation1(F) & object(x))). relation1(e). relation1(conceivable). relation1(nonegreater). relation2(greaterthan). (all x (object(x) -> (exemplifies1(nonegreater,x) <-> exemplifies1(conceivable,x) & -(exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))). (exists x (object(x) & exemplifies1(nonegreater,x))). (exists x (object(x) & exemplifies1(nonegreater,x))) -> (exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y = x))))). (all F (relation1(F) -> ((exists x (object(x) & exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x))))) -> (exists x (object(x) & is_the(x,F)))))). (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))). (all x (object(x) -> (is_the(x,nonegreater) & -exemplifies1(e,x) -> (exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))). is_the(g,nonegreater). end_of_list. formulas(goals). 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 x (object(x) -> -relation1(x))) # label(non_clause). [assumption]. 2 (all x (object(x) -> -relation2(x))) # label(non_clause). [assumption]. 3 (all F (relation1(F) -> -relation2(F))) # label(non_clause). [assumption]. 4 (all x all F (exemplifies1(F,x) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 5 (all x all y all R (exemplifies2(R,x,y) -> relation2(R) & object(x) & object(y))) # label(non_clause). [assumption]. 6 (all x all F (is_the(x,F) -> relation1(F) & object(x))) # label(non_clause). [assumption]. 7 (all x (object(x) -> (exemplifies1(nonegreater,x) <-> exemplifies1(conceivable,x) & -(exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))) # label(non_clause). [assumption]. 8 (exists x (object(x) & exemplifies1(nonegreater,x))) # label(non_clause). [assumption]. 9 (exists x (object(x) & exemplifies1(nonegreater,x))) -> (exists x (object(x) & exemplifies1(nonegreater,x) & (all y (object(y) -> (exemplifies1(nonegreater,y) -> y = x))))) # label(non_clause). [assumption]. 10 (all F (relation1(F) -> ((exists x (object(x) & exemplifies1(F,x) & (all y (object(y) -> (exemplifies1(F,y) -> y = x))))) -> (exists x (object(x) & is_the(x,F)))))) # label(non_clause). [assumption]. 11 (all F (relation1(F) -> ((exists x (object(x) & is_the(x,F))) -> (all y (object(y) -> (is_the(y,F) -> exemplifies1(F,y))))))) # label(non_clause). [assumption]. 12 (all x (object(x) -> (is_the(x,nonegreater) & -exemplifies1(e,x) -> (exists y (object(y) & exemplifies2(greaterthan,y,x) & exemplifies1(conceivable,y)))))) # label(non_clause). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -object(x) | -relation1(x). -object(x) | -relation2(x). -relation1(x) | -relation2(x). -exemplifies1(x,y) | relation1(x). -exemplifies1(x,y) | object(y). -exemplifies2(x,y,z) | relation2(x). -exemplifies2(x,y,z) | object(y). -exemplifies2(x,y,z) | object(z). -is_the(x,y) | relation1(y). -is_the(x,y) | object(x). relation1(e). relation1(conceivable). relation1(nonegreater). relation2(greaterthan). -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(conceivable,x). -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies2(greaterthan,y,x) | -exemplifies1(conceivable,y). -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | object(f1(x)). -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies2(greaterthan,f1(x),x). -object(x) | exemplifies1(nonegreater,x) | -exemplifies1(conceivable,x) | exemplifies1(conceivable,f1(x)). object(c1). exemplifies1(nonegreater,c1). -object(x) | -exemplifies1(nonegreater,x) | object(c2). -object(x) | -exemplifies1(nonegreater,x) | exemplifies1(nonegreater,c2). -object(x) | -exemplifies1(nonegreater,x) | -object(y) | -exemplifies1(nonegreater,y) | y = c2. -relation1(x) | -object(y) | -exemplifies1(x,y) | object(f2(x,y)) | object(f3(x)). -relation1(x) | -object(y) | -exemplifies1(x,y) | object(f2(x,y)) | is_the(f3(x),x). -relation1(x) | -object(y) | -exemplifies1(x,y) | exemplifies1(x,f2(x,y)) | object(f3(x)). -relation1(x) | -object(y) | -exemplifies1(x,y) | exemplifies1(x,f2(x,y)) | is_the(f3(x),x). -relation1(x) | -object(y) | -exemplifies1(x,y) | f2(x,y) != y | object(f3(x)). -relation1(x) | -object(y) | -exemplifies1(x,y) | f2(x,y) != y | is_the(f3(x),x). -relation1(x) | -object(y) | -is_the(y,x) | -object(z) | -is_the(z,x) | exemplifies1(x,z). -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | object(f4(x)). -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies2(greaterthan,f4(x),x). -object(x) | -is_the(x,nonegreater) | exemplifies1(e,x) | exemplifies1(conceivable,f4(x)). is_the(g,nonegreater). end_of_list. ============================== end of clauses for search ============= % The maximum domain element in the input is 0. ============================== DOMAIN SIZE 2 ========================= ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=111, kept=111. Selections=1, assignments=2, propagations=54, current_models=0. Rewrite_terms=140, rewrite_bools=314, indexes=50. Rules_from_neg_clauses=8, cross_offs=8. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== MODEL ================================= % Model 1 at 0.01 seconds. conceivable : 0 e : 0 g : 2 greaterthan : 1 nonegreater : 0 c1 : 2 c2 : 2 f1 : 0 1 2 --------- 0 0 0 f3 : 0 1 2 --------- 2 0 0 f4 : 0 1 2 --------- 0 0 0 f2 : | 0 1 2 --+------ 0 | 0 0 0 1 | 0 0 0 2 | 0 0 0 object : 0 1 2 --------- 0 0 1 relation1 : 0 1 2 --------- 1 0 0 relation2 : 0 1 2 --------- 0 1 0 exemplifies1 : | 0 1 2 --+------ 0 | 0 0 1 1 | 0 0 0 2 | 0 0 0 is_the : | 0 1 2 --+------ 0 | 0 0 0 1 | 0 0 0 2 | 1 0 0 exemplifies2(0,0,0) = 0. exemplifies2(0,0,1) = 0. exemplifies2(0,0,2) = 0. exemplifies2(0,1,0) = 0. exemplifies2(0,1,1) = 0. exemplifies2(0,1,2) = 0. exemplifies2(0,2,0) = 0. exemplifies2(0,2,1) = 0. exemplifies2(0,2,2) = 0. exemplifies2(1,0,0) = 0. exemplifies2(1,0,1) = 0. exemplifies2(1,0,2) = 0. exemplifies2(1,1,0) = 0. exemplifies2(1,1,1) = 0. exemplifies2(1,1,2) = 0. exemplifies2(1,2,0) = 0. exemplifies2(1,2,1) = 0. exemplifies2(1,2,2) = 0. exemplifies2(2,0,0) = 0. exemplifies2(2,0,1) = 0. exemplifies2(2,0,2) = 0. exemplifies2(2,1,0) = 0. exemplifies2(2,1,1) = 0. exemplifies2(2,1,2) = 0. exemplifies2(2,2,0) = 0. exemplifies2(2,2,1) = 0. exemplifies2(2,2,2) = 0. ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=259, kept=259. Selections=21, assignments=24, propagations=60, current_models=1. Rewrite_terms=307, rewrite_bools=408, indexes=40. Rules_from_neg_clauses=5, cross_offs=11. ============================== end of statistics ===================== User_CPU=0.01, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 20589 exit (max_models) Fri Jul 27 15:11:40 2007 The process finished Fri Jul 27 15:11:40 2007