Aussagenlogik | Grundresolution und Herbrand-Strukture

Question

Aufgabe:

Gegeben sei die folgende prädikatenlogische Skolemformel φ, deren Matrixformel bereits in KNF ist.

Problem/Ansatz:

Hallo, wie löse ich am besten diese Aufgabe? Vielen Dank im voraus.