============================== Mace4 ================================= Mace4 (32) version June-2007, June 2007. Process 5076 was started by zalta on mally, Sat Jul 14 18:08:32 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 Sum(x,x) = x). (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))). (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 Sum(x,x) = x) # label(non_clause). [assumption]. 3 (all x all y all z Sum(Sum(x,y),z) = Sum(x,Sum(y,z))) # label(non_clause). [assumption]. 4 (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). Sum(x,x) = x. Sum(Sum(x,y),z) = Sum(x,Sum(y,z)). -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 1 f1 : | 0 1 --+---- 0 | 0 0 1 | 0 1 IsIn : | 0 1 --+---- 0 | 1 0 1 | 1 1 ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=26, kept=21. Selections=3, assignments=3, propagations=9, current_models=1. Rewrite_terms=41, rewrite_bools=26, indexes=1. Rules_from_neg_clauses=2, cross_offs=2. ============================== end of statistics ===================== User_CPU=0.00, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 5076 exit (max_models) Sat Jul 14 18:08:32 2007 The process finished Sat Jul 14 18:08:32 2007