%
% 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 graineating 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}".
(exists x exists y
(animal(x) &
animal(y) &
(exists z (Grain(z) &
eats(y,z) &
eats(x,y))))).
end_of_list.