- ∀ x (Hound(x) → Howl(x))
- ∀ x ∀ y (Have (x,y) ∧ Cat (y) → ¬ ∃ z (Have(x,z) ∧
Mice(z)))
- ∀ x (Light Sleepers(x) → ¬ ∃ y (Have (x,y) ∧
Howl(y)))
- ∃ x (Have (John,x) ∧ (Cat(x) ∨ Hound(x)))
- Light Sleepers(John) → ¬ ∃ z (Have(John,z) ∧
Mice(z))
The set of CNF clauses for this problem is thus as follows:
- ¬ Hound(x) ∨ Howl(x)
- ¬ Have(x,y) ∨ ¬ Cat(y) ∨ ¬ Have(x,z) ∨ ¬ Mice(z)
- ¬ Light Sleepers(x) ∨ ¬ Have(x,y) ∨ ¬ Howl(y)
-
- Have(John,a)
- Cat(a) ∨ Hound(a)
-
- Light Sleepers(John)
- Have(John,b)
- Mice(b)