----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Aug 19 14:47:20 2003 The command was "../../bin/mace2 -n11 -x -m1000". list(usable). 1 [] f(x,x)=x. 2 [] f(f(f(x,y),x),y)=x. 3 [] f(f(f(x,y),y),f(x,y))=x. 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(z,x)!=u|f(u,y)=x. 3 [] f(x,y)!=z|f(z,y)!=u|f(u,z)=x. end_of_list. --- Starting search for models of size 11 --- Adding basic QG constraints on last column of f. function f quasigroup. 49787 clauses were generated; 31819 of those survived the first stage of unit preprocessing; there are 1452 atoms. After all unit preprocessing, 755 atoms are still unassigned; 18944 clauses remain; 300 of those are non-Horn (selectable); 4924 K allocated; cpu time so far for this domain size: 0.03 sec.  The search is complete. No models were found. ----- statistics for domain size 11 ---- Input: Clauses input 31819 Literal occurrences input 79461 Greatest atom 1452 Unit preprocess: Preprocess unit assignments 697 Clauses after subsumption 18944 Literal occ. after subsump. 49569 Selectable clauses 300 Decide: Splits 291 Unit assignments 41021 Failed paths 292 Memory: Memory malloced 42 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.02 DPLL 0.07 ======================================= Total times for run (seconds): user CPU time 0.09 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) The search is complete. No models were found. The job finished Tue Aug 19 14:47:20 2003