----- MACE 2.2, August 2003 -----
The process was started by mccune on gyro.thornwood,
Tue Aug 19 14:47:13 2003
The command was "../../bin/mace2 -n4 -m50".

list(usable).
1 [] a(a(L,x),y)=a(x,a(y,y)).
2 [] a(a(a(Q,x),y),z)=a(y,a(x,z)).
end_of_list.

formula_list(usable).
-(exists Q all x (a(Q,x)=a(x,a(Q,x)))).
end_of_list.

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

list(usable).
3 [] a(x1,$f1(x1))!=a($f1(x1),a(x1,$f1(x1))).
end_of_list.

list(flattened_and_parted_clauses).
1 [] a(x,x)!=y|a(z,y)!=u|$Connect2(x,z,u).
1 [] a(x,y)=z| -$Connect1(u,x)| -$Connect2(y,u,z).
1 [] L!=x|a(x,y)!=z|$Connect1(y,z).
2 [] a(x,y)!=z|a(u,z)!=v|$Connect4(x,y,u,v).
2 [] a(x,y)=z| -$Connect3(u,v,x)| -$Connect4(u,y,v,z).
2 [] Q!=x|a(x,y)!=z|$Connect5(y,z).
2 [] a(x,y)!=z|$Connect3(u,y,z)| -$Connect5(u,x).
3 [] a(x,y)!=z|$f1(x)!=y| -$Connect6(y,z).
3 [] a(x,y)!=z|y!=z|$Connect6(x,y).
end_of_list.

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

Applying isomorphism constraints to constants: L Q.

3244 clauses were generated; 3144 of those survived the first stage
of unit preprocessing; there are 536 atoms.

After all unit preprocessing, 516 atoms are still unassigned;
3124 clauses remain; 22 of those are non-Horn (selectable);
4897 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.

Exit by max_models parameter.  The set is satisfiable (50 model(s) found).


----- statistics for domain size 4 ----
Input:
    Clauses input                  3144
    Literal occurrences input      9234
    Greatest atom                   536
Unit preprocess:
    Preprocess unit assignments      20
    Clauses after subsumption      3124
    Literal occ. after subsump.    9214
    Selectable clauses               22
Decide:
    Splits                          122
    Unit assignments               9673
    Failed paths                     65
Memory:
    Memory malloced                15 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.00
    DPLL                           0.00

=======================================
Total times for run (seconds):
    user CPU time                  0.01   (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)

Exit by max_models parameter.  The set is satisfiable (50 model(s) found).

The job finished Tue Aug 19 14:47:13 2003