============================== Mace4 ================================= Mace4 (32) version 2009-02A, February 2009. Process 11176 was started by mccune on cleo, Wed Feb 25 09:31:58 2009 The command was "/home/mccune/bin/mace4 -f qg.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file qg.in assign(domain_size,5). % assign(domain_size, 5) -> assign(start_size, 5). % assign(domain_size, 5) -> assign(end_size, 5). assign(max_models,-1). clear(print_models). formulas(assumptions). x * (x \ y) = y. x \ (x * y) = y. (x / y) * y = x. (x * y) / y = x. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). x * (x \ y) = y. x \ (x * y) = y. (x / y) * y = x. (x * y) / y = x. end_of_list. ============================== end of clauses for search ============= % There are no natural numbers in the input. ============================== DOMAIN SIZE 5 ========================= Model 1 has been found. Model 10 has been found. Model 100 has been found. Model 1000 has been found. Model 10000 has been found. ============================== STATISTICS ============================ For domain size 5. Current CPU time: 0.00 seconds (total CPU time: 0.44 seconds). Ground clauses: seen=100, kept=100. Selections=10691, assignments=53390, propagations=319455, current_models=10944. Rewrite_terms=946380, rewrite_bools=468844, indexes=199567. Rules_from_neg_clauses=119888, cross_offs=246763. ============================== end of statistics ===================== User_CPU=0.44, System_CPU=0.00, Wall_clock=1. Exiting with 10944 models. Process 11176 exit (all_models) Wed Feb 25 09:31:59 2009 The process finished Wed Feb 25 09:31:59 2009