----- MACE 2.2f, August 2004 -----
The process was started by mccune on gyro.thornwood,
Mon Aug  2 15:44:30 2004
The command was "../../bin/mace2 -n4 -m1000".
op(400,xfx,*).

formula_list(usable).
all x y z ((x*y)*z=x* (y*z)).
all x y z (x*y<x*z->y<z).
all x y z (y*x<z*x->y<z).
end_of_list.

-------> usable clausifies to:

list(usable).
1 [] (x*y)*z=x* (y*z).
2 [] -(x*y<x*z)|y<z.
3 [] -(y*x<z*x)|y<z.
end_of_list.

list(flattened_and_parted_clauses).
1 [] x*y!=z|u*z!=v|$Connect1(x,y,u,v).
1 [] x*y!=z|z*u=v| -$Connect1(y,u,x,v).
2 [] x*y!=z| -(u<z)|$Connect2(x,y,u).
2 [] x*y!=z|y<u| -$Connect2(x,u,z).
3 [] x*y!=z| -(u<z)|$Connect3(x,y,u).
3 [] x*y!=z|x<u| -$Connect3(u,y,z).
end_of_list.

--- Starting search for models of size 4 ---


3216 clauses were generated; 2688 of those survived the first stage
of unit preprocessing; there are 480 atoms.

After all unit preprocessing, 448 atoms are still unassigned;
2656 clauses remain; 16 of those are non-Horn (selectable);
4895 K allocated; cpu time so far for this domain size: 0.00 sec.

The 1st model has been found.

The 10th model has been found.

The 100th model has been found.

The search is complete.  The set is satisfiable (386 model(s) found).


----- statistics for domain size 4 ----
Input:
    Clauses input                  2688
    Literal occurrences input      7392
    Greatest atom                   480
Unit preprocess:
    Preprocess unit assignments      32
    Clauses after subsumption      2656
    Literal occ. after subsump.    7360
    Selectable clauses               16
Decide:
    Splits                          509
    Unit assignments              52475
    Failed paths                    124
Memory:
    Memory malloced                13 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.00
    DPLL                           0.02

=======================================
Total times for run (seconds):
    user CPU time                  0.02   (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.  The set is satisfiable (386 model(s) found).

The job finished Mon Aug  2 15:44:30 2004