============================== Mace4 ================================= Mace4 (32) version 22-May-2007, May 2007. Process 26979 was started by mccune on cleo, Tue May 22 14:44:22 2007 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))) # label(non_clause). [assumption]. 2 (all x (Fox(x) -> animal(x))) # label(non_clause). [assumption]. 3 (all x (Bird(x) -> animal(x))) # label(non_clause). [assumption]. 4 (all x (Caterpillar(x) -> animal(x))) # label(non_clause). [assumption]. 5 (all x (Snail(x) -> animal(x))) # label(non_clause). [assumption]. 6 (all x (Grain(x) -> plant(x))) # label(non_clause). [assumption]. 7 (exists x Wolf(x)) # label(non_clause). [assumption]. 8 (exists x Fox(x)) # label(non_clause). [assumption]. 9 (exists x Bird(x)) # label(non_clause). [assumption]. 10 (exists x Caterpillar(x)) # label(non_clause). [assumption]. 11 (exists x Snail(x)) # label(non_clause). [assumption]. 12 (exists x Grain(x)) # label(non_clause). [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))))) # label(non_clause). [assumption]. 14 (all x all y (Caterpillar(x) & Bird(y) -> Smaller(x,y))) # label(non_clause). [assumption]. 15 (all x all y (Snail(x) & Bird(y) -> Smaller(x,y))) # label(non_clause). [assumption]. 16 (all x all y (Bird(x) & Fox(y) -> Smaller(x,y))) # label(non_clause). [assumption]. 17 (all x all y (Fox(x) & Wolf(y) -> Smaller(x,y))) # label(non_clause). [assumption]. 18 (all x all y (Bird(x) & Caterpillar(y) -> eats(x,y))) # label(non_clause). [assumption]. 19 (all x (Caterpillar(x) -> (exists y (plant(y) & eats(x,y))))) # label(non_clause). [assumption]. 20 (all x all y (Wolf(x) & Fox(y) -> -eats(x,y))) # label(non_clause). [assumption]. 21 (all x all y (Wolf(x) & Grain(y) -> -eats(x,y))) # label(non_clause). [assumption]. 22 (all x all y (Bird(x) & Snail(y) -> -eats(x,y))) # label(non_clause). [assumption]. 23 -(exists x exists y (animal(x) & animal(y) & eats(x,y) & (all z (Grain(z) -> eats(y,z))))) # label(non_clause). [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.01 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.01, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 26979 exit (max_models) Tue May 22 14:44:22 2007 The process finished Tue May 22 14:44:22 2007