1. 2 klauzule, vypsat vsechny ktere jsou odvodit 1 aplikaci rezolucniho nebo faktorizacniho pravidla, 20b
2. 1 klauzule, zaskrtnout z vyberu ty ktere subsumuje, 15b
3. prevest na klauzule, 15b

   ((∀X)(∃Y)p(X,Y)) ⇔ ((∃X)(∀Y)q(X,Y))

4. teorie + hypoteza dokazat pomoci tableaux, 20b
5. najit vsechny neisomorfni dvouprvkove modely, 30b

∗ je funkce, ~ je relace
(one ∗ apple) ~ one
(one ∗ one) ~ apple
¬(one ~ apple)
(∀X)(X ~ X)