===== Zkouška AU 13.6.2017=====

  - 2 klauzule, vypsat vsechny ktere jsou odvodit 1 aplikaci rezolucniho nebo faktorizacniho pravidla, 20b
  - 1 klauzule, zaskrtnout z vyberu ty ktere subsumuje, 15b
  - prevest na klauzule, 15b <code>((∀X)(∃Y)p(X,Y)) ⇔ ((∃X)(∀Y)q(X,Y))</code>
  - teorie + hypoteza dokazat pomoci tableaux, 20b
  - najit vsechny neisomorfni dvouprvkove modely, 30b

<code>
∗ je funkce, ~ je relace
(one ∗ apple) ~ one
(one ∗ one) ~ apple
¬(one ~ apple)
(∀X)(X ~ X)
</code>

~~DISCUSSION~~