----- MACE4 2005-A, 30 June 2005 ----- Built with library LADR July-2005, 30 June 2005. The process was started by mccune on theorem.mcs.anl.gov, Tue Jul 5 21:30:24 2005 The command was "../bin/mace4". The process ID is 8593. assign(iterate_up_to,10). set(verbose). 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. % Finished reading the input. % There are no domain elements in the input. === Starting model search for domain size 2. === Initial partial model: $c1 : - $c2 : - $c3 : - $c4 : - $c5 : - $c6 : - $f1 : 0 1 ------- - - $f2 : | 0 1 --+---- 0 | - - 1 | - - Wolf : 0 1 ------- - - animal : 0 1 ------- - - Fox : 0 1 ------- - - Bird : 0 1 ------- - - Caterpillar : 0 1 ------- - - Snail : 0 1 ------- - - Grain : 0 1 ------- - - plant : 0 1 ------- - - eats : | 0 1 --+---- 0 | - - 1 | - - Smaller : | 0 1 --+---- 0 | - - 1 | - - --------- statistics for domain size 2 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=78, kept=78. Selections=6, assignments=11, propagations=99, current_models=0. Rewrite_terms=35, rewrite_bools=533, indexes=27. Rules_from_neg_clauses=16, cross_offs=16. === Starting model search for domain size 3. === Initial partial model: $c1 : - $c2 : - $c3 : - $c4 : - $c5 : - $c6 : - $f1 : 0 1 2 --------- - - - $f2 : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - Wolf : 0 1 2 --------- - - - animal : 0 1 2 --------- - - - Fox : 0 1 2 --------- - - - Bird : 0 1 2 --------- - - - Caterpillar : 0 1 2 --------- - - - Snail : 0 1 2 --------- - - - Grain : 0 1 2 --------- - - - plant : 0 1 2 --------- - - - eats : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - Smaller : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - -------- Model 1 at 0.02 seconds -------- $c1 : 0 $c2 : 0 $c3 : 0 $c4 : 1 $c5 : 0 $c6 : 0 $f1 : 0 1 2 --------- 0 0 0 $f2 : | 0 1 2 --+------ 0 | 0 2 0 1 | 0 0 0 2 | 0 0 0 Wolf : 0 1 2 --------- 1 0 0 animal : 0 1 2 --------- 1 1 0 Fox : 0 1 2 --------- 1 0 0 Bird : 0 1 2 --------- 1 0 0 Caterpillar : 0 1 2 --------- 0 1 0 Snail : 0 1 2 --------- 1 0 0 Grain : 0 1 2 --------- 1 0 1 plant : 0 1 2 --------- 1 0 1 eats : | 0 1 2 --+------ 0 | 0 1 0 1 | 1 0 0 2 | 0 0 0 Smaller : | 0 1 2 --+------ 0 | 1 0 0 1 | 1 0 0 2 | 0 0 0 -------- end of model -------- --------- statistics for domain size 3 --------- Current CPU time: 0.01 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=201, kept=201. Selections=28, assignments=29, propagations=32, current_models=1. Rewrite_terms=31, rewrite_bools=477, indexes=13. Rules_from_neg_clauses=1, cross_offs=7. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 359 359 0 0.0 K string_buf ( 8) 341 341 0 0.0 K token ( 20) 687 687 0 0.0 K pterm ( 16) 357 357 0 0.0 K ilist ( 8) 78 78 0 0.0 K plist ( 8) 1664 1448 216 1.7 K mlist ( 12) 71 71 0 0.0 K term ( 16) 5792 5560 232 3.6 K term arg arrays: 0.6 K literal ( 12) 62 0 62 0.7 K clause ( 32) 25 0 25 0.8 K clist_pos ( 20) 0 0 0 0.0 K clist ( 16) 0 0 0 0.0 K mclause ( 20) 279 279 0 0.0 K (7.5 K high) mstate ( 16) 42 42 0 0.0 K jnode ( 28) 238 238 0 0.0 K estack (3208) 42 42 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (0.05 megs used). List 1, length 15, 0.1 K List 2, length 203, 1.6 K List 4, length 14, 0.2 K List 5, length 542, 10.6 K List 6, length 462, 10.8 K List 7, length 32, 0.9 K List 8, length 78, 2.4 K List 9, length 12, 0.4 K List 10, length 3, 0.1 K List 11, length 18, 0.8 K List 12, length 36, 1.7 K List 13, length 24, 1.2 K List 26, length 46, 4.7 K User_CPU=0.02, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 8593 exit (max_models) Tue Jul 5 21:30:24 2005 The process finished Tue Jul 5 21:30:24 2005