============================== Mace4 =================================
Mace4 (32) version 22-May-2007, May 2007.
Process 26983 was started by mccune on cleo,
Tue May 22 14:44:27 2007
The command was "/home/mccune/bin/mace4 -f kauer.in".
============================== end of head ===========================

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

% Reading from file kauer.in

assign(iterate_up_to,10).

formulas(theory).
(all x exists y x < y).
(all x all y (x < y -> -(y < x))).
(all x all y (x < y -> (exists z (x < z & z < y)))).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 (all x exists y x < y) # label(non_clause).  [assumption].
2 (all x all y (x < y -> -(y < x))) # label(non_clause).  [assumption].
3 (all x all y (x < y -> (exists z (x < z & z < y)))) # label(non_clause).  [assumption].

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

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

formulas(mace4_clauses).
x < f1(x).
-(x < y) | -(y < x).
-(x < y) | x < f2(x,y).
-(x < y) | f2(x,y) < y.
end_of_list.

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

% The maximum domain element in the input is 0.

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

NOTE: unsatisfiability detected on input.

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=6, kept=4.
Selections=0, assignments=0, propagations=6, current_models=0.
Rewrite_terms=2, rewrite_bools=4, indexes=2.
Rules_from_neg_clauses=2, cross_offs=2.

============================== 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=30, kept=24.
Selections=1, assignments=2, propagations=12, current_models=0.
Rewrite_terms=5, rewrite_bools=32, indexes=3.
Rules_from_neg_clauses=3, cross_offs=9.

============================== 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=52, kept=44.
Selections=2, assignments=5, propagations=22, current_models=0.
Rewrite_terms=14, rewrite_bools=66, indexes=6.
Rules_from_neg_clauses=6, cross_offs=23.

============================== 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=80, kept=70.
Selections=3, assignments=9, propagations=19, current_models=0.
Rewrite_terms=15, rewrite_bools=62, indexes=7.
Rules_from_neg_clauses=2, cross_offs=24.

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

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

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

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=114, kept=102.
Selections=4, assignments=14, propagations=29, current_models=0.
Rewrite_terms=26, rewrite_bools=96, indexes=12.
Rules_from_neg_clauses=3, cross_offs=45.

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

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

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

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

        function(f1(_), [ 1, 2, 3, 1, 0, 0, 0 ]),

        function(f2(_,_), [
			   0, 3, 1, 2, 0, 0, 0,
			   0, 0, 4, 0, 6, 0, 2,
			   0, 0, 0, 6, 0, 3, 5,
			   0, 5, 0, 0, 1, 4, 0,
			   5, 0, 0, 0, 0, 2, 0,
			   6, 0, 0, 0, 0, 0, 1,
			   4, 0, 0, 0, 3, 0, 0 ]),

        relation(<(_,_), [
			   0, 1, 1, 1, 0, 0, 0,
			   0, 0, 1, 0, 1, 0, 1,
			   0, 0, 0, 1, 0, 1, 1,
			   0, 1, 0, 0, 1, 1, 0,
			   1, 0, 1, 0, 0, 1, 0,
			   1, 1, 0, 0, 0, 0, 1,
			   1, 0, 0, 1, 1, 0, 0 ])
]).

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

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

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=154, kept=140.
Selections=39, assignments=60, propagations=68, current_models=1.
Rewrite_terms=119, rewrite_bools=250, indexes=23.
Rules_from_neg_clauses=17, cross_offs=137.

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

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

Exiting with 1 model.

Process 26983 exit (max_models) Tue May 22 14:44:27 2007
The process finished Tue May 22 14:44:27 2007