============================== Mace4 ================================= Mace4 (32) version June-2007, June 2007. Process 4906 was started by zalta on mally, Sat Jul 14 17:19:17 2007 The command was "mace -c -N 8 -p 1". ============================== end of head =========================== ============================== INPUT ================================= formulas(sos). (all x all y Sum(x,y) = Sum(y,x)). (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = 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 ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y Sum(x,y) = Sum(y,x)) # label(non_clause). [assumption]. 2 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). Sum(x,y) = Sum(y,x). -IsIn(x,y) | Sum(x,f1(x,y)) = y. IsIn(x,y) | Sum(x,z) != y. 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. Sum : | 0 1 --+---- 0 | 0 0 1 | 0 0 f1 : | 0 1 --+---- 0 | 0 0 1 | 0 0 IsIn : | 0 1 --+---- 0 | 1 0 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=16, kept=16. Selections=7, assignments=7, propagations=5, current_models=1. Rewrite_terms=24, rewrite_bools=22, indexes=0. 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 4906 exit (max_models) Sat Jul 14 17:19:17 2007 The process finished Sat Jul 14 17:19:17 2007