Ejemplo Otter

% steam.in

%                Schubert's Steamroller

% 

% Wolves, foxes, birds, caterpillars, and snails are animals,

% and there are some of each of them.

% 

% Also there are some grains, and grains are plants.

% 

% Every animal either likes to eat all plants or all animals much

% smaller than itself that like to eat some plants.

% 

% Caterpillars and snails are much smaller than birds, which are much

% smaller than foxes, which are in turn much smaller than wolves.

% 

% Wolves do not like to eat foxes or grains, while birds like to eat

% caterpillars but not snails.

% 

% Caterpillars and snails like to eat some plants.

% 

% Prove there is an animal that likes to eat a grain-eating animal.

%

set(auto).

formula_list(usable).

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 animals either eat all plants or eat all smaller animals that eat some plants.

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 (Snail(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)).

% negation of "there is an animal that eats {an animal that eats all grains}".

% Note the answer literal, which records the predator and the prey.

-(exists x exists y ( -$answer(eats(x,y)) &

        animal(x) &

        animal(y) &

        eats(x,y) &

               (all z (Grain(z) -> eats(y,z))))).

end_of_list.