============================== Mace4 =================================
Mace4 (32) version June-2006C, June 2006.
Process 13042 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:31 2006
The command was "/home/mccune/bin/mace4 -f qg.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file qg.in

assign(domain_size,5).
assign(max_models,- 1).
clear(print_models_portable).

clauses(theory).
x * (x \ y) = y.
x \ (x * y) = y.
(x / y) * y = x.
(x * y) / y = x.
end_of_list.

============================== end of input ==========================

% The maximum domain element in the input is 0.

============================== DOMAIN SIZE 5 =========================

Model 1 has been found.

Model 10 has been found.

Model 100 has been found.

Model 1000 has been found.

Model 10000 has been found.

============================== STATISTICS ============================

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.36 seconds).
Ground clauses: seen=100, kept=100.
Selections=10691, assignments=53390, propagations=319455, current_models=10944.
Rewrite_terms=946380, rewrite_bools=468844, indexes=199567.
Rules_from_neg_clauses=119888, cross_offs=246763.

============================== end of statistics =====================

User_CPU=0.36, System_CPU=0.00, Wall_clock=0.

Exiting with 10944 models.

Process 13042 exit (all_models) Mon Jun 19 16:40:31 2006
The process finished Mon Jun 19 16:40:31 2006