Zaškrtávací, vybrat formule, které lze z množiny 2 formulí získat jednou aplikací pravidla rezoluce nebo faktorizace. Valná většina byla správně nezaškrtnutá.

Zaškrtávací, z pěti formulí vybrat dvojice formulí, které se subsumují. (Pozn. U subsumpce a rezoluce dejte pozor, že při unifikaci jsou stejně pojmenované proměnné z různých klauzulí ve skutečnosti různé.)

Upravit formuli s kvantifikátory a ekvivalencí na množinu klauzulí.

Pro teorii najít všechny modely velikosti 2. Teorie byla myslím:

Pro teorii z předchozího příkladu vysvětlit, jak úlohu hledání modelu převést na SAT a jak z řešení SAT zpětně zkonstruovat model.