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

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

% Reading from file steam.in

assign(iterate_up_to,10).

formulas(theory).
(all x (Wolf(x) -> animal(x))).
(all x (Fox(x) -> animal(x))).
(all x (Bird(x) -> animal(x))).
(all x (Caterpillar(x) -> animal(x))).
(all x (Snail(x) -> animal(x))).
(all x (Grain(x) -> plant(x))).
(exists x (Wolf(x))).
(exists x (Fox(x))).
(exists x (Bird(x))).
(exists x (Caterpillar(x))).
(exists x (Snail(x))).
(exists x (Grain(x))).
(all x (animal(x) -> (all y (plant(y) -> eats(x,y))) | (all z (animal(z) & Smaller(z,x) & (exists u (plant(u) & eats(z,u))) -> eats(x,z))))).
(all x all y (Caterpillar(x) & Bird(y) -> Smaller(x,y))).
(all x all y (Snail(x) & Bird(y) -> Smaller(x,y))).
(all x all y (Bird(x) & Fox(y) -> Smaller(x,y))).
(all x all y (Fox(x) & Wolf(y) -> Smaller(x,y))).
(all x all y (Bird(x) & Caterpillar(y) -> eats(x,y))).
(all x (Caterpillar(x) -> (exists y (plant(y) & eats(x,y))))).
(all x all y (Wolf(x) & Fox(y) -> - eats(x,y))).
(all x all y (Wolf(x) & Grain(y) -> - eats(x,y))).
(all x all y (Bird(x) & Snail(y) -> - eats(x,y))).
- (exists x exists y (animal(x) & animal(y) & eats(x,y) & (all z (Grain(z) -> eats(y,z))))).
end_of_list.

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

% The maximum domain element in the input is 0.

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

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=78, kept=78.
Selections=11, assignments=22, propagations=196, current_models=0.
Rewrite_terms=70, rewrite_bools=1048, indexes=54.
Rules_from_neg_clauses=32, cross_offs=32.

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

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

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

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

        function(c1, [ 0]),

        function(c2, [ 0]),

        function(c3, [ 0]),

        function(c4, [ 1]),

        function(c5, [ 0]),

        function(c6, [ 0]),

        function(f1(_), [ 0, 0, 0]),

        function(f2(_,_), [ 0, 2, 0,
			   0, 0, 0,
			   0, 0, 0]),

        relation(Bird(_), [ 1, 0, 0]),

        relation(Caterpillar(_), [ 0, 1, 0]),

        relation(Fox(_), [ 1, 0, 0]),

        relation(Grain(_), [ 1, 0, 1]),

        relation(Snail(_), [ 1, 0, 0]),

        relation(Wolf(_), [ 1, 0, 0]),

        relation(animal(_), [ 1, 1, 0]),

        relation(plant(_), [ 1, 0, 1]),

        relation(Smaller(_,_), [ 1, 0, 0,
			   1, 0, 0,
			   0, 0, 0]),

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

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

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

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=201, kept=201.
Selections=31, assignments=32, propagations=29, current_models=1.
Rewrite_terms=31, rewrite_bools=474, indexes=13.
Rules_from_neg_clauses=1, cross_offs=7.

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

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

Exiting with 1 model.

Process 13046 exit (max_models) Mon Jun 19 16:40:33 2006
The process finished Mon Jun 19 16:40:33 2006