blob: 1d890af7d4f979d5d3c2b50ee53d2b6f034cdba8 (
plain)
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
34
35
|
;; IVY operation: PROVE
;;
;; Schubert's Steamroller.
(imp (and (all x (imp (Wolf x) (animal x)))
(all x (imp (Fox x) (animal x)))
(all x (imp (Bird x) (animal x)))
(all x (imp (Snail x) (animal x)))
(all x (imp (Grain x) (plant x)))
(exists x (Wolf x))
(exists x (Fox x))
(exists x (Bird x))
(exists x (Snail x))
(exists x (Grain x))
(all x (all y (imp (and (Snail x) (Bird y)) (Smaller x y))))
(all x (all y (imp (and (Bird x) (Fox y)) (Smaller x y))))
(all x (all y (imp (and (Fox x) (Wolf y)) (Smaller x y))))
(all x (imp (Snail x) (exists y (and (plant y) (eats x y)))))
(all x (all y (imp (and (Wolf x) (Fox y)) (not (eats x y)))))
(all x (all y (imp (and (Wolf x) (Grain y)) (not (eats x y)))))
(all x (all y (imp (and (Bird x) (Snail y)) (not (eats x y)))))
(all x (imp (animal x)
(or (all y (imp (plant y) (eats x y)))
(all z (imp (and (animal z)
(Smaller z x)
(exists u (and (plant u)
(eats z u))))
(eats x z)))))))
(exists x (exists y (and (animal x)
(animal y)
(eats x y)
(all z (imp (grain z) (eats y z)))))))
|
