============================== Mace4 ================================= Mace4 (32) version August-2006A, August 2006. Process 10704 was started by mccune on cleo.thornwood, Sat Aug 12 20:58:13 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 ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x (Wolf(x) -> animal(x))). [assumption]. 2 (all x (Fox(x) -> animal(x))). [assumption]. 3 (all x (Bird(x) -> animal(x))). [assumption]. 4 (all x (Caterpillar(x) -> animal(x))). [assumption]. 5 (all x (Snail(x) -> animal(x))). [assumption]. 6 (all x (Grain(x) -> plant(x))). [assumption]. 7 (exists x (Wolf(x))). [assumption]. 8 (exists x (Fox(x))). [assumption]. 9 (exists x (Bird(x))). [assumption]. 10 (exists x (Caterpillar(x))). [assumption]. 11 (exists x (Snail(x))). [assumption]. 12 (exists x (Grain(x))). [assumption]. 13 (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))))). [assumption]. 14 (all x all y (Caterpillar(x) & Bird(y) -> Smaller(x,y))). [assumption]. 15 (all x all y (Snail(x) & Bird(y) -> Smaller(x,y))). [assumption]. 16 (all x all y (Bird(x) & Fox(y) -> Smaller(x,y))). [assumption]. 17 (all x all y (Fox(x) & Wolf(y) -> Smaller(x,y))). [assumption]. 18 (all x all y (Bird(x) & Caterpillar(y) -> eats(x,y))). [assumption]. 19 (all x (Caterpillar(x) -> (exists y (plant(y) & eats(x,y))))). [assumption]. 20 (all x all y (Wolf(x) & Fox(y) -> -eats(x,y))). [assumption]. 21 (all x all y (Wolf(x) & Grain(y) -> -eats(x,y))). [assumption]. 22 (all x all y (Bird(x) & Snail(y) -> -eats(x,y))). [assumption]. 23 -(exists x exists y (animal(x) & animal(y) & eats(x,y) & (all z (Grain(z) -> eats(y,z))))). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -Wolf(x) | animal(x). -Fox(x) | animal(x). -Bird(x) | animal(x). -Caterpillar(x) | animal(x). -Snail(x) | animal(x). -Grain(x) | plant(x). Wolf(c1). Fox(c2). Bird(c3). Caterpillar(c4). Snail(c5). Grain(c6). -animal(x) | -plant(y) | eats(x,y) | -animal(z) | -Smaller(z,x) | -plant(u) | -eats(z,u) | eats(x,z). -Caterpillar(x) | -Bird(y) | Smaller(x,y). -Snail(x) | -Bird(y) | Smaller(x,y). -Bird(x) | -Fox(y) | Smaller(x,y). -Fox(x) | -Wolf(y) | Smaller(x,y). -Bird(x) | -Caterpillar(y) | eats(x,y). -Caterpillar(x) | plant(f1(x)). -Caterpillar(x) | eats(x,f1(x)). -Wolf(x) | -Fox(y) | -eats(x,y). -Wolf(x) | -Grain(y) | -eats(x,y). -Bird(x) | -Snail(y) | -eats(x,y). -animal(x) | -animal(y) | -eats(x,y) | Grain(f2(x,y)). -animal(x) | -animal(y) | -eats(x,y) | -eats(y,f2(x,y)). end_of_list. ============================== end of clauses for search ============= % 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=223, current_models=0. Rewrite_terms=74, rewrite_bools=1181, indexes=62. Rules_from_neg_clauses=40, cross_offs=40. ============================== 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 10704 exit (max_models) Sat Aug 12 20:58:13 2006 The process finished Sat Aug 12 20:58:13 2006