/usr/share/doc/prover9-doc/examples/PUZ031-1.in is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 | set(prolog_style_variables).
formulas(assumptions).
animal(X) | -wolf(X) # label(wolf_is_an_animal) # label(axiom).
animal(X) | -fox(X) # label(fox_is_an_animal) # label(axiom).
animal(X) | -bird(X) # label(bird_is_an_animal) # label(axiom).
animal(X) | -caterpillar(X) # label(caterpillar_is_an_animal) # label(axiom).
animal(X) | -snail(X) # label(snail_is_an_animal) # label(axiom).
wolf(a_wolf) # label(there_is_a_wolf) # label(axiom).
fox(a_fox) # label(there_is_a_fox) # label(axiom).
bird(a_bird) # label(there_is_a_bird) # label(axiom).
caterpillar(a_caterpillar) # label(there_is_a_caterpillar) # label(axiom).
snail(a_snail) # label(there_is_a_snail) # label(axiom).
grain(a_grain) # label(there_is_a_grain) # label(axiom).
plant(X) | -grain(X) # label(grain_is_a_plant) # label(axiom).
eats(Animal,Plant) | eats(Animal,Small_animal) | -animal(Animal) | -plant(Plant) | -animal(Small_animal) | -plant(Other_plant) | -much_smaller(Small_animal,Animal) | -eats(Small_animal,Other_plant) # label(eating_habits) # label(axiom).
much_smaller(Catapillar,Bird) | -caterpillar(Catapillar) | -bird(Bird) # label(caterpillar_smaller_than_bird) # label(axiom).
much_smaller(Snail,Bird) | -snail(Snail) | -bird(Bird) # label(snail_smaller_than_bird) # label(axiom).
much_smaller(Bird,Fox) | -bird(Bird) | -fox(Fox) # label(bird_smaller_than_fox) # label(axiom).
much_smaller(Fox,Wolf) | -fox(Fox) | -wolf(Wolf) # label(fox_smaller_than_wolf) # label(axiom).
-wolf(Wolf) | -fox(Fox) | -eats(Wolf,Fox) # label(wolf_dont_eat_fox) # label(axiom).
-wolf(Wolf) | -grain(Grain) | -eats(Wolf,Grain) # label(wolf_dont_eat_grain) # label(axiom).
eats(Bird,Catapillar) | -bird(Bird) | -caterpillar(Catapillar) # label(bird_eats_caterpillar) # label(axiom).
-bird(Bird) | -snail(Snail) | -eats(Bird,Snail) # label(bird_dont_eat_snail) # label(axiom).
plant(caterpillar_food_of(Catapillar)) | -caterpillar(Catapillar) # label(caterpillar_food_is_a_plant) # label(axiom).
eats(Catapillar,caterpillar_food_of(Catapillar)) | -caterpillar(Catapillar) # label(caterpillar_eats_caterpillar_food) # label(axiom).
plant(snail_food_of(Snail)) | -snail(Snail) # label(snail_food_is_a_plant) # label(axiom).
eats(Snail,snail_food_of(Snail)) | -snail(Snail) # label(snail_eats_snail_food) # label(axiom).
-animal(Animal) | -animal(Grain_eater) | -grain(Grain) | -eats(Animal,Grain_eater) | -eats(Grain_eater,Grain) # label(prove_the_animal_exists) # label(negated_conjecture).
end_of_list.
formulas(goals).
end_of_list.
|