Description

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 in turn are 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. Which animal likes to eat a grain eating animal, and which?

ProverBox Specification (download file)

CONST OBJ : TYPE
      animal, wolf, fox, bird, caterpillar, snail, grain, plant : PRED[OBJ]
      eats, much_smaller : PRED[OBJ, OBJ]
      caterpillar_food_of, snail_food_of : [OBJ -> OBJ]
      a_wolf, a_fox, a_bird, a_caterpillar, a_snail, a_grain : OBJ

VAR X, Animal, Plant, Small_animal, Other_plant, Caterpillar, Bird,
    Snail, Fox, Wolf, Grain : OBJ

AXIOM wolf_is_an_animal: animal(X) or not wolf(X)

AXIOM fox_is_an_animal: animal(X) or not fox(X)

AXIOM bird_is_an_animal: animal(X) or not bird(X)

AXIOM caterpillar_is_an_animal: animal(X) or not caterpillar(X)

AXIOM snail_is_an_animal: animal(X) or not snail(X)

AXIOM there_is_a_wolf: wolf(a_wolf)

AXIOM there_is_a_fox: fox(a_fox)

AXIOM there_is_a_bird: bird(a_bird)

AXIOM there_is_a_caterpillar: caterpillar(a_caterpillar)

AXIOM there_is_a_snail: snail(a_snail)

AXIOM there_is_a_grain: grain(a_grain)

AXIOM grain_is_a_plant: plant(X) or not grain(X)

AXIOM eating_habits: eats(Animal,Plant) or eats(Animal,Small_animal)
        or not animal(Animal) or not plant(Plant)
        or not animal(Small_animal) or not plant(Other_plant)
        or not much_smaller(Small_animal,Animal)
        or not eats(Small_animal,Other_plant)

AXIOM caterpillar_smaller_than_bird: much_smaller(Caterpillar,Bird)
        or not caterpillar(Caterpillar) or not bird(Bird)

AXIOM snail_smaller_than_bird: much_smaller(Snail,Bird)
        or not snail(Snail) or not bird(Bird)

AXIOM bird_smaller_than_fox: much_smaller(Bird,Fox)
        or not bird(Bird) or not fox(Fox)

AXIOM fox_smaller_than_wolf: much_smaller(Fox,Wolf)
        or not fox(Fox) or not wolf(Wolf)

AXIOM wolf_dont_eat_fox: not wolf(Wolf) or not fox(Fox)
        or not eats(Wolf,Fox)

AXIOM wolf_dont_eat_grain: not wolf(Wolf) or not grain(Grain)
        or not eats(Wolf,Grain)

AXIOM bird_eats_caterpillar: eats(Bird,Caterpillar) or not bird(Bird)
        or not caterpillar(Caterpillar)

AXIOM bird_dont_eat_snail: not bird(Bird) or not snail(Snail)
        or not eats(Bird,Snail)

AXIOM caterpillar_food_is_a_plant: plant(caterpillar_food_of(Caterpillar))
        or not caterpillar(Caterpillar)

AXIOM caterpillar_eats_caterpillar_food:
        eats(Caterpillar,caterpillar_food_of(Caterpillar))
        or not caterpillar(Caterpillar)

AXIOM snail_food_is_a_plant: plant(snail_food_of(Snail))
        or not snail(Snail)

AXIOM snail_eats_snail_food: eats(Snail,snail_food_of(Snail))
        or not snail(Snail)

THEOREM prove_the_animal_exists: exists Predator:OBJ,Food:OBJ,
          Grain_eater:OBJ.
          animal(Predator) and animal(Grain_eater) and grain(Food)
          and eats(Predator,Grain_eater) and eats(Grain_eater,Food)