----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Aug 19 14:47:19 2003 The command was "../../bin/mace2 -n7 -x -m1000". list(usable). 1 [] f(x,x)=x. 2 [] f(x,y)!=u|f(z,w)!=u|f(v,x)!=y|f(v,z)!=w|x=z|y=w. end_of_list. list(mace_constraints). 0 [] property(f(_,_),quasigroup). end_of_list. list(flattened_and_parted_clauses). 1 [] f(x,x)=x. 2 [] f(x,y)!=z|f(u,v)!=z|x=u|y=v| -$Connect1(x,y,u,v). 2 [] f(x,y)!=z|f(x,u)!=v|$Connect1(y,z,u,v). end_of_list. --- Starting search for models of size 7 --- Adding basic QG constraints on last column of f. function f quasigroup. 36919 clauses were generated; 12677 of those survived the first stage of unit preprocessing; there are 2793 atoms. After all unit preprocessing, 2563 atoms are still unassigned; 9787 clauses remain; 120 of those are non-Horn (selectable); 4961 K allocated; cpu time so far for this domain size: 0.01 sec. The 1st model has been found. The 10th model has been found.  The search is complete. The set is satisfiable (14 model(s) found). ----- statistics for domain size 7 ---- Input: Clauses input 12677 Literal occurrences input 34943 Greatest atom 2793 Unit preprocess: Preprocess unit assignments 230 Clauses after subsumption 9787 Literal occ. after subsump. 27718 Selectable clauses 120 Decide: Splits 361 Unit assignments 49450 Failed paths 348 Memory: Memory malloced 79 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.03 ======================================= Total times for run (seconds): user CPU time 0.04 (0 hr, 0 min, 0 sec) system CPU time 0.01 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) The search is complete. The set is satisfiable (14 model(s) found). The job finished Tue Aug 19 14:47:19 2003