Aufgabe 18 b): Die folgende Formel ist auf Unerfüllbarkeit zu testen:

F = ∀x : (¬B(x) ∨ K(x)) ∧ ∀y : (¬∀z : (¬R(y, z) ∨ K(z)) ∧ ¬∃u : (R(y, u) ∧ ¬B(u))) ∨ A(y))
∧∀v : (¬∃w : (R(v, w) ∧ B(w)) ∨ B(v)) ∧ ∀t : ¬A(t)
≡ ∀x : (¬B(x) ∨ K(x)) ∧ ∀y : ((∃z : (R(y, z) ∧ ¬K(z)) ∧ ∀u : (¬R(y, u) ∨ B(u))) ∨ A(y))
∧∀v : (∀w : (¬R(v, w) ∨ ¬B(w)) ∨ B(v)) ∧ ∀t : ¬A(t)
≡ ∀y : ∃z : ∀u : ∀x : ∀v : ∀w : ∀t : ((((R(y, z) ∧ ¬K(z)) ∧ (¬R(y, u) ∨ B(u))) ∨ A(y))
∧(¬B(x) ∨ K(x)) ∧ (¬R(v, w) ∨ ¬B(w) ∨ B(v)) ∧ ¬A(t))
∼ ∀y : ∀u : ∀x : ∀v : ∀w : ∀t : ((R(y, f(y)) ∨ A(y)) ∧ (¬K(f(y)) ∨ A(y)) ∧ (¬R(y, u) ∨ B(u) ∨ A(y))
∧(¬B(x) ∨ K(x)) ∧ (¬R(v, w) ∨ ¬B(w) ∨ B(v)) ∧ ¬A(t)) [z ↦ f(y)]

Daraus erhält man

κ = {{R(y, f(y)), A(y))}, {¬K(f(y)), A(y))}, {¬R(y, u), B(u), A(y)}, {¬B(x), K(x)},
{¬R(v, w), ¬B(w), B(v)}, {¬A(t)}}

[figure: {R(y, f(y)), A(y)}; {¬A(t)}; t↦y; {R(y, f(y))}; (1)]

[figure: {¬R(y, u), B(u), A(y)}; {¬A(t)}; t↦y; {¬R(y, u), B(u)}; (2)]

[figure: {¬K(f(y)), A(y)}; {¬A(t)}; t↦y; {¬K(f(y))}; (3)]

[figure: {R(y, f(y))}(1); {¬R(y, u), B(u)}(2); u↦f(y); {B(f(y))}; (4)]

[figure: {¬B(x), K(x)}; x↦f(y); {B(f(y))}(4); {K(f(y))}; {¬K(f(y))}(3); ∅]

Die Formel ist unerfüllbar, mithin ist es unmöglich, die Regeln des Spiels zu erfüllen.