Pliki wykl01-klas.j, lab01-klas.j oraz lab02-klas.j zawierają sekwenty wymagające użycia reguły niewprost lub równoważnej definiującej logikę klasyczną. Pliki RZ-kl.j oraz RZ-kl.jp również zawierają stwierdzenia klasycznego rachunku zdań wraz z dowodami.
Celem tego zadania jest tym razem udowodnienie, że logika klasyczna jest niezbędna do wyprowadzenia tych zdań. Tzn. celem jest wykonanie akcji ,,disprove'' i zbudowanie struktury Kripkego pokazującej, że nie są to twierdzenia rachunku intuicjonistycznego.