1.
(a)
waiting > godot.
tick /\ waiting > waiting.
tick.
(b) godot 1

waiting 2

tick, waiting 3

waiting 4
 looping here.
(c) Prolog loops and does not return.
(d) decision procedure would return false (godot is not provable).
2.
(a)
even(z).
all x. even(x) > odd(s(x)).
all x. odd(x) > even(s(x)).
(b)
exists x. odd(x) /\ even(x).
(c): first and 3rd are models; second is not: (s(s(z)) is even,
s(s(s(z))) is not odd.
(d): not logical consequence since there is a model (M1) where
it is false.
(e) ~ exists x. odd(x) /\ even(x) not logical consequence, since
it is false in M3 above.
(f) exists x.odd(x) is logical consequence:
Prolog shows odd(s(z)), Prolog proof is sound, ie proved statements
are true in all models