============================== Mace4 =================================
Mace4 (32) version August-2006A, August 2006.
Process 10615 was started by mccune on cleo.thornwood,
Sat Aug 12 20:57:29 2006
The command was "/home/mccune/bin/mace4 -f cand10.in".
============================== end of head ===========================

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

% Reading from file cand10.in

assign(iterate_up_to,100).

formulas(theory).
f(f(g(f(x,x)),y),g(f(g(f(x,f(x,z))),y))) = z.
f(f(A,B),C) != f(A,f(B,C)).
f(g(x),x) = 1.
f(x,g(x)) = 1.
f(g(x),f(x,y)) = y.
f(f(y,x),g(x)) = y.
f(1,x) = x.
f(x,1) = x.
g(g(x)) = x.
g(1) = 1.
end_of_list.

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

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:

============================== end of process non-clausal formulas ===

============================== CLAUSES FOR SEARCH ====================

formulas(mace4_clauses).
f(f(g(f(x,x)),y),g(f(g(f(x,f(x,z))),y))) = z.
f(f(A,B),C) != f(A,f(B,C)).
f(g(x),x) = 1.
f(x,g(x)) = 1.
f(g(x),f(x,y)) = y.
f(f(x,y),g(y)) = x.
f(1,x) = x.
f(x,1) = x.
g(g(x)) = x.
g(1) = 1.
end_of_list.

============================== end of clauses for search =============

% The maximum domain element in the input is 1.

============================== DOMAIN SIZE 2 =========================

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=28, kept=22.
Selections=7, assignments=14, propagations=6, current_models=0.
Rewrite_terms=161, rewrite_bools=29, indexes=4.
Rules_from_neg_clauses=3, cross_offs=3.

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

============================== DOMAIN SIZE 3 =========================

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=62, kept=58.
Selections=14, assignments=42, propagations=15, current_models=0.
Rewrite_terms=538, rewrite_bools=100, indexes=36.
Rules_from_neg_clauses=5, cross_offs=12.

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

============================== DOMAIN SIZE 4 =========================

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

For domain size 4.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=118, kept=114.
Selections=49, assignments=188, propagations=130, current_models=0.
Rewrite_terms=5253, rewrite_bools=904, indexes=288.
Rules_from_neg_clauses=23, cross_offs=56.

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

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

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

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=202, kept=198.
Selections=87, assignments=393, propagations=419, current_models=0.
Rewrite_terms=8893, rewrite_bools=1331, indexes=1095.
Rules_from_neg_clauses=105, cross_offs=412.

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

============================== DOMAIN SIZE 6 =========================

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=320, kept=316.
Selections=278, assignments=1523, propagations=1716, current_models=0.
Rewrite_terms=70673, rewrite_bools=10888, indexes=4743.
Rules_from_neg_clauses=428, cross_offs=1867.

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

============================== DOMAIN SIZE 7 =========================

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=478, kept=474.
Selections=413, assignments=2507, propagations=3384, current_models=0.
Rewrite_terms=94752, rewrite_bools=11395, indexes=14869.
Rules_from_neg_clauses=648, cross_offs=5734.

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

============================== DOMAIN SIZE 8 =========================

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

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=682, kept=678.
Selections=1213, assignments=8765, propagations=14386, current_models=0.
Rewrite_terms=605044, rewrite_bools=78445, indexes=71915.
Rules_from_neg_clauses=3218, cross_offs=22280.

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

============================== DOMAIN SIZE 9 =========================

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

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.32 seconds).
Ground clauses: seen=938, kept=934.
Selections=2464, assignments=20142, propagations=36349, current_models=0.
Rewrite_terms=1250140, rewrite_bools=141288, indexes=244516.
Rules_from_neg_clauses=6680, cross_offs=76026.

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

============================== DOMAIN SIZE 10 ========================

============================== MODEL =================================

interpretation( 10, [number=1, seconds=0], [

        function(A, [ 0]),

        function(B, [ 2]),

        function(C, [ 4]),

        function(g(_), [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9]),

        function(f(_,_), [ 1, 0, 3, 2, 5, 4, 8, 9, 6, 7,
			   0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
			   3, 2, 1, 0, 6, 9, 4, 8, 7, 5,
			   2, 3, 0, 1, 7, 8, 9, 4, 5, 6,
			   5, 4, 6, 7, 1, 0, 2, 3, 9, 8,
			   4, 5, 9, 8, 0, 1, 7, 6, 3, 2,
			   8, 6, 4, 9, 2, 7, 1, 5, 0, 3,
			   9, 7, 8, 4, 3, 6, 5, 1, 2, 0,
			   6, 8, 7, 5, 9, 3, 0, 2, 1, 4,
			   7, 9, 5, 6, 8, 2, 3, 0, 4, 1])
]).

============================== end of model ==========================

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.56 seconds).
Ground clauses: seen=1252, kept=1248.
Selections=2307, assignments=22935, propagations=44291, current_models=1.
Rewrite_terms=1417947, rewrite_bools=220824, indexes=304820.
Rules_from_neg_clauses=7279, cross_offs=128871.

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

User_CPU=0.56, System_CPU=0.00, Wall_clock=1.

Exiting with 1 model.

Process 10615 exit (max_models) Sat Aug 12 20:57:30 2006
The process finished Sat Aug 12 20:57:30 2006