----- 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