From 9477dbe667f250ecd23f8fc0d56b942191526421 Mon Sep 17 00:00:00 2001
From: Franciszek Malinka <franciszek.malinka@gmail.com>
Date: Thu, 25 Feb 2021 14:42:55 +0100
Subject: Stare semestry, niepoukladane

---
 .../compiled/drracket/errortrace/prop_rkt.dep      |   1 +
 .../compiled/drracket/errortrace/prop_rkt.zo       | Bin 0 -> 1709 bytes
 .../compiled/drracket/errortrace/props_rkt.dep     |   1 +
 .../compiled/drracket/errortrace/props_rkt.zo      | Bin 0 -> 3273 bytes
 .../compiled/drracket/errortrace/solution_rkt.dep  |   1 +
 .../compiled/drracket/errortrace/solution_rkt.zo   | Bin 0 -> 10868 bytes
 .../compiled/drracket/errortrace/props_rkt.dep     |   1 +
 .../compiled/drracket/errortrace/props_rkt.zo      | Bin 0 -> 3273 bytes
 Semestr 2/racket/lista5/julita/props.rkt           |  52 +++++++
 Semestr 2/racket/lista5/julita/solution.bak        | 164 +++++++++++++++++++++
 Semestr 2/racket/lista5/julita/solution.rkt        | 164 +++++++++++++++++++++
 Semestr 2/racket/lista5/prop.rkt                   |   1 +
 Semestr 2/racket/lista5/props.bak                  |  71 +++++++++
 Semestr 2/racket/lista5/props.rkt                  |  52 +++++++
 Semestr 2/racket/lista5/skrr/solution.bak          | 135 +++++++++++++++++
 Semestr 2/racket/lista5/skrr/solution.rkt          |  88 +++++++++++
 Semestr 2/racket/lista5/sol2.rkt                   |  90 +++++++++++
 Semestr 2/racket/lista5/solution.bak               | 135 +++++++++++++++++
 Semestr 2/racket/lista5/solution.rkt               | 140 ++++++++++++++++++
 Semestr 2/racket/lista5/xd.bak                     |   4 +
 Semestr 2/racket/lista5/xd.rkt                     |   4 +
 21 files changed, 1104 insertions(+)
 create mode 100644 Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep
 create mode 100644 Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo
 create mode 100644 Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep
 create mode 100644 Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo
 create mode 100644 Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep
 create mode 100644 Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo
 create mode 100644 Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep
 create mode 100644 Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo
 create mode 100644 Semestr 2/racket/lista5/julita/props.rkt
 create mode 100644 Semestr 2/racket/lista5/julita/solution.bak
 create mode 100644 Semestr 2/racket/lista5/julita/solution.rkt
 create mode 100644 Semestr 2/racket/lista5/prop.rkt
 create mode 100644 Semestr 2/racket/lista5/props.bak
 create mode 100644 Semestr 2/racket/lista5/props.rkt
 create mode 100644 Semestr 2/racket/lista5/skrr/solution.bak
 create mode 100644 Semestr 2/racket/lista5/skrr/solution.rkt
 create mode 100644 Semestr 2/racket/lista5/sol2.rkt
 create mode 100644 Semestr 2/racket/lista5/solution.bak
 create mode 100644 Semestr 2/racket/lista5/solution.rkt
 create mode 100644 Semestr 2/racket/lista5/xd.bak
 create mode 100644 Semestr 2/racket/lista5/xd.rkt

(limited to 'Semestr 2/racket/lista5')

diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep
new file mode 100644
index 0000000..6e0cfbb
--- /dev/null
+++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep	
@@ -0,0 +1 @@
+("7.6" racket ("f0a57e86828cdab35eaad454d5deb80353172518" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt"))
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo
new file mode 100644
index 0000000..748fec9
Binary files /dev/null and b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo differ
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep
new file mode 100644
index 0000000..0926afc
--- /dev/null
+++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep	
@@ -0,0 +1 @@
+("7.6" racket ("e0347fa7e89f59bc97c197db02b440f666222428" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt"))
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo
new file mode 100644
index 0000000..eccc7f7
Binary files /dev/null and b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo differ
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep
new file mode 100644
index 0000000..9810b4c
--- /dev/null
+++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep	
@@ -0,0 +1 @@
+("7.6" racket ("ae3a6974cdd4582f480927d9968aad2f495b7fc4" . "33b0c09c14dce6a2115d810ac3d0f25a9dce3205") #"C:\\Users\\franc\\Documents\\lista5\\props.rkt" (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt"))
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo
new file mode 100644
index 0000000..ca1ab20
Binary files /dev/null and b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo differ
diff --git a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep
new file mode 100644
index 0000000..0926afc
--- /dev/null
+++ b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep	
@@ -0,0 +1 @@
+("7.6" racket ("e0347fa7e89f59bc97c197db02b440f666222428" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt"))
diff --git a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo
new file mode 100644
index 0000000..eccc7f7
Binary files /dev/null and b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo differ
diff --git a/Semestr 2/racket/lista5/julita/props.rkt b/Semestr 2/racket/lista5/julita/props.rkt
new file mode 100644
index 0000000..204b108
--- /dev/null
+++ b/Semestr 2/racket/lista5/julita/props.rkt	
@@ -0,0 +1,52 @@
+#lang racket
+
+(provide conj conj-left conj-right conj?
+         disj disj-left disj-right disj?
+         neg neg-subf neg?
+         var?)
+
+
+(define (conj p q)
+  (list 'conj p q))
+
+(define (conj-left f)
+  (second f))
+
+(define (conj-right f)
+  (third f))
+
+(define (conj? t)
+  (and (list? t)
+        (= 3 (length t))
+        (eq? 'conj (car t))))
+
+
+(define (disj p q)
+  (list 'disj p q))
+
+(define (disj-left f)
+  (second f))
+
+(define (disj-right f)
+  (third f))
+
+(define (disj? t)
+  (and (list? t)
+        (= 3 (length t))
+        (eq? 'disj (car t))))
+
+
+(define (neg x)
+  (list 'neg x))
+
+(define (neg-subf x)
+  (second x))
+
+(define (neg? t)
+  (and (list? t)
+        (= 2 (length t))
+        (eq? 'neg (car t))))
+
+
+(define (var? t)
+  (symbol? t))
diff --git a/Semestr 2/racket/lista5/julita/solution.bak b/Semestr 2/racket/lista5/julita/solution.bak
new file mode 100644
index 0000000..b3dda94
--- /dev/null
+++ b/Semestr 2/racket/lista5/julita/solution.bak	
@@ -0,0 +1,164 @@
+#lang racket
+
+;;Praca grupowa:
+;;Dawid Holewa
+;;Julita Osman
+;;Aleksandra Stępniewska
+
+(require "props.rkt")
+(provide falsifiable-cnf?)
+
+;Ponieważ formuła w cnf to konjunkcja klauzul
+;a klauzula to alternatywa literałów
+;to formuła w tej postaci jest tautologią
+;wtedy i tylko wtedy gdy
+;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami)
+;w przeciwnym razie, formulę taką da się zanegować;
+;zatem nasz pomysł polega na tym, aby
+;1)sprawdzic czy formula jest tautologia
+;2)jesli tak to zwracamy fałsz
+;3)wpp. pierwsza z klauzul, która nie jest tautologia
+;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf)
+;"przesuwamy" na początek listy reprezentującej cnf
+
+;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie
+;możemy skorzystać z własności alternatywy
+;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją
+
+;Falsifiable, która sprawdza każde wartościowania
+;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań,
+;podczas gdy
+;falsifiable, która opiera się na strukturze cnf 
+;przechodzi po cnf, aż do napotkania pierwszej
+;mozliwej do zanegowania klauzuli
+;zatem w najroszym przypadku przejdziemy po całym cnf
+;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli
+;zauważmy,ze jeśli formuła jest tautologią to oszczędzamy bardzo dużo czasu nie rozpartując wszystkich wartosciowań, tylko wypisujac odrazu falsz
+
+;Ta druga jest więc efektywniejsza
+
+(define (lit? f);; a lub ~a
+  (or (var? f) ;;a
+      (and (neg? f);;~a 
+           (var? (neg-subf f)))))
+
+(define (lit-pos v)
+  v)
+
+(define (lit-neg v)
+  (neg v))
+
+(define (lit-var l) ;;a-->a      ~a-->a
+  (if (var? l)
+      l
+      (neg-subf l)))
+
+(define (lit-pos? l)
+  (var? l))
+
+(define (to-nnf f)
+  (cond
+    [(var? f)  (lit-pos f)]
+    [(neg? f)  (to-nnf-neg (neg-subf f))]
+    [(conj? f) (conj (to-nnf (conj-left f))
+                     (to-nnf (conj-right f)))]
+    [(disj? f) (disj (to-nnf (disj-left f))
+                     (to-nnf (disj-right f)))]))
+
+(define (to-nnf-neg f)
+  (cond
+    [(var? f)  (lit-neg f)]
+    [(neg? f)  (to-nnf (neg-subf f))]
+    [(conj? f) (disj (to-nnf-neg (conj-left f))
+                     (to-nnf-neg (conj-right f)))]
+    [(disj? f) (conj (to-nnf-neg (disj-left f))
+                     (to-nnf-neg (disj-right f)))]))
+
+(define (mk-cnf xss)
+  (cons 'cnf xss))
+
+(define (clause? f)
+  (and (list? f)
+       (andmap lit? f)))
+
+(define (cnf? f)
+  (and (pair? f)
+       (eq? 'cnf (car f))
+       (list? (cdr f))
+       (andmap clause? (cdr f))))
+
+(define (to-cnf f)
+  (define (join xss yss)
+    (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss)))
+
+  (define (go f)
+    (cond
+      [(lit? f)  (list (list f))]
+      [(conj? f) (append (go (conj-left f))
+                         (go (conj-right f)))]
+      [(disj? f) (join (go (disj-left f))
+                       (go (disj-right f)))]))
+  (mk-cnf (go f)))
+
+
+(define (contain-both-literals?  claus)
+  (define (aux to-check)
+    (cond [(empty? to-check) #f]
+          [(neg? (car to-check))
+           (if (memq (neg-subf (car to-check)) claus)
+               #t
+               (aux (cdr to-check)))]
+          [else (aux (cdr to-check))]))
+  (aux claus))
+
+
+;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf 
+;; zawiera chociaz jedną parę zmiennej i jej negacji
+;; zwraca liste pusta jesli cnf jest tautologia
+;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg)
+(define (has-both big-set)
+  (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek
+    (define x-ty (list-ref big-set x))
+    (append (list x-ty) (remove x-ty big-set)))
+  (define (aux iter big-set)
+  (if (= iter (length big-set))
+      '()
+      (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie
+          (aux (+ iter 1) big-set)
+          (possible-to-neg big-set iter))))
+  (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf
+          
+
+(define (falsifiable-cnf? t)
+  (define tt (to-cnf (to-nnf t)))
+  (define f (has-both tt))
+  (if (empty? f)
+      #f
+      (find-valuation f)))
+            
+
+(define (valuate f sigma)
+  (define (insigma-proc lista result)
+    (cond [(null? lista) result]
+          [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))]))
+  ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli:   
+  (define insigma (insigma-proc sigma '()))
+  (define (aux insigma otherclause sigma)
+    (cond [(null? otherclause) sigma]
+          [(if (memq (lit-var (car otherclause)) insigma)
+               (aux insigma (cdr otherclause) sigma)
+               (if(neg? (car otherclause))
+                  (aux (append insigma (list(car otherclause)))
+                    (cdr otherclause)
+                    (append sigma (list(list (lit-var(car otherclause)) 1))))
+                  (aux (append insigma (list(car otherclause)))
+                    (cdr otherclause)
+                    (append sigma (list(list (car otherclause) 0))))))]))
+  (if (empty? f)
+      sigma
+      (valuate (cdr f)
+                    (aux insigma (car f) sigma))))
+
+(define (find-valuation f)
+  (valuate f '())) 
+
diff --git a/Semestr 2/racket/lista5/julita/solution.rkt b/Semestr 2/racket/lista5/julita/solution.rkt
new file mode 100644
index 0000000..da87bf9
--- /dev/null
+++ b/Semestr 2/racket/lista5/julita/solution.rkt	
@@ -0,0 +1,164 @@
+#lang racket
+
+;;Praca grupowa:
+;;Dawid Holewa
+;;Julita Osman
+;;Aleksandra Stępniewska
+
+(require "props.rkt")
+(provide falsifiable-cnf?)
+
+;Ponieważ formuła w cnf to konjunkcja klauzul
+;a klauzula to alternatywa literałów
+;to formuła w tej postaci jest tautologią
+;wtedy i tylko wtedy gdy
+;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami)
+;w przeciwnym razie, formulę taką da się zanegować;
+;zatem nasz pomysł polega na tym, aby
+;1)sprawdzic czy formula jest tautologia
+;2)jesli tak to zwracamy fałsz
+;3)wpp. pierwsza z klauzul, która nie jest tautologia
+;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf)
+;"przesuwamy" na początek listy reprezentującej cnf
+
+;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie
+;możemy skorzystać z własności alternatywy
+;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją
+
+;Falsifiable, która sprawdza każde wartościowania
+;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań,
+;podczas gdy
+;falsifiable, która opiera się na strukturze cnf 
+;przechodzi po cnf, aż do napotkania pierwszej
+;mozliwej do zanegowania klauzuli
+;zatem w najroszym przypadku przejdziemy po całym cnf
+;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli
+;zauważmy,ze jeśli formuła jest tautologią to oszczędzamy bardzo dużo czasu nie rozpartując wszystkich wartosciowań, tylko wypisujac odrazu falsz
+
+;Ta druga jest więc efektywniejsza
+
+(define (lit? f);; a lub ~a
+  (or (var? f) ;;a
+      (and (neg? f);;~a 
+           (var? (neg-subf f)))))
+
+(define (lit-pos v)
+  v)
+
+(define (lit-neg v)
+  (neg v))
+
+(define (lit-var l) ;;a-->a      ~a-->a
+  (if (var? l)
+      l
+      (neg-subf l)))
+
+(define (lit-pos? l)
+  (var? l))
+
+(define (to-nnf f)
+  (cond
+    [(var? f)  (lit-pos f)]
+    [(neg? f)  (to-nnf-neg (neg-subf f))]
+    [(conj? f) (conj (to-nnf (conj-left f))
+                     (to-nnf (conj-right f)))]
+    [(disj? f) (disj (to-nnf (disj-left f))
+                     (to-nnf (disj-right f)))]))
+
+(define (to-nnf-neg f)
+  (cond
+    [(var? f)  (lit-neg f)]
+    [(neg? f)  (to-nnf (neg-subf f))]
+    [(conj? f) (disj (to-nnf-neg (conj-left f))
+                     (to-nnf-neg (conj-right f)))]
+    [(disj? f) (conj (to-nnf-neg (disj-left f))
+                     (to-nnf-neg (disj-right f)))]))
+
+(define (mk-cnf xss)
+  (cons 'cnf xss))
+
+(define (clause? f)
+  (and (list? f)
+       (andmap lit? f)))
+
+(define (cnf? f)
+  (and (pair? f)
+       (eq? 'cnf (car f))
+       (list? (cdr f))
+       (andmap clause? (cdr f))))
+
+(define (to-cnf f)
+  (define (join xss yss)
+    (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss)))
+
+  (define (go f)
+    (cond
+      [(lit? f)  (list (list f))]
+      [(conj? f) (append (go (conj-left f))
+                         (go (conj-right f)))]
+      [(disj? f) (join (go (disj-left f))
+                       (go (disj-right f)))]))
+  (mk-cnf (go f)))
+
+
+(define (contain-both-literals?  claus)
+  (define (aux to-check)
+    (cond [(empty? to-check) #f]
+          [(neg? (car to-check))
+           (if (memq (neg-subf (car to-check)) claus)
+               #t
+               (aux (cdr to-check)))]
+          [else (aux (cdr to-check))]))
+  (aux claus))
+
+
+;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf 
+;; zawiera chociaz jedną parę zmiennej i jej negacji
+;; zwraca liste pusta jesli cnf jest tautologia
+;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg)
+(define (has-both big-set)
+  (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek
+    (define x-ty (list-ref big-set x))
+    (append (list x-ty) (remove x-ty big-set)))
+  (define (aux iter big-set)
+  (if (= iter (length big-set))
+      '()
+      (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie
+          (aux (+ iter 1) big-set)
+          (possible-to-neg big-set iter))))
+  (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf
+          
+
+(define (falsifiable-cnf? t)
+  (define tt (to-cnf (to-nnf t)))
+  (define f (has-both tt))
+  (if (empty? f)
+      #f
+      (find-valuation f)))
+            
+
+(define (valuate f sigma)
+  (define (insigma-proc lista result)
+    (cond [(null? lista) result]
+          [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))]))
+  ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli:   
+  (define insigma (insigma-proc sigma '()))
+  (define (aux insigma otherclause sigma)
+    (cond [(null? otherclause) sigma]
+          [(if (memq (lit-var (car otherclause)) insigma)
+               (aux insigma (cdr otherclause) sigma)
+               (if(neg? (car otherclause))
+                  (aux (append insigma (list(car otherclause)))
+                    (cdr otherclause)
+                    (append sigma (list(list (lit-var(car otherclause)) true))))
+                  (aux (append insigma (list(car otherclause)))
+                    (cdr otherclause)
+                    (append sigma (list(list (car otherclause) false))))))]))
+  (if (empty? f)
+      sigma
+      (valuate (cdr f)
+                    (aux insigma (car f) sigma))))
+
+(define (find-valuation f)
+  (valuate f '())) 
+
diff --git a/Semestr 2/racket/lista5/prop.rkt b/Semestr 2/racket/lista5/prop.rkt
new file mode 100644
index 0000000..6f1f7b4
--- /dev/null
+++ b/Semestr 2/racket/lista5/prop.rkt	
@@ -0,0 +1 @@
+#lang racket
diff --git a/Semestr 2/racket/lista5/props.bak b/Semestr 2/racket/lista5/props.bak
new file mode 100644
index 0000000..1a5659a
--- /dev/null
+++ b/Semestr 2/racket/lista5/props.bak	
@@ -0,0 +1,71 @@
+#lang racket
+
+(provide var?
+         neg?
+         conj?
+         disj?
+         conj
+         disj
+         neg
+         conj-left
+         conj-right
+         disj-right
+         disj-left
+         neg-subf)
+; (require "solution.rkt")
+
+(define (var? t) (symbol? t))
+
+(define (neg? t)
+  (and (list? t)
+       (= 2 (length t))
+       (eq? 'neg (car t))))
+
+(define (conj? t)
+  (and (list? t)
+       (= 3 (length t))
+       (eq? 'conj (car t))))
+
+(define (disj? t)
+  (and (list? t)
+       (= 3 (length t))
+       (eq? 'disj (car t))))
+
+(define (lit? t)
+  (or (var? t)
+      (and (neg? t)
+           (var? (neg-subf t)))))
+
+(define (conj left right)
+  (list 'conj left right))
+
+(define (disj left right)
+  (list 'disj left right))
+
+(define (neg f)
+  (list 'neg f))
+
+(define (conj-left f)
+  (if (conj? f)
+      (cadr f)
+      (error "Złe dane ze znacznikiem -- CONJ-LEFT" f)))
+
+(define (conj-right f)
+  (if (conj? f)
+      (caddr f)
+      (error "Złe dane ze znacznikiem -- CONJ-RIGHT" f)))
+
+(define (disj-left f)
+  (if (disj? f)
+      (cadr f)
+      (error "Złe dane ze znacznikiem -- DISJ-LEFT" f)))
+
+(define (disj-right f)
+  (if (disj? f)
+      (caddr f)
+      (error "Złe dane ze znacznikiem -- DISJ-RIGHT" f)))
+
+(define (neg-subf f)
+  (if (neg? f)
+      (cadr f)
+      (error "Złe dane ze znacznikiem -- NEG-FORM" f)))
diff --git a/Semestr 2/racket/lista5/props.rkt b/Semestr 2/racket/lista5/props.rkt
new file mode 100644
index 0000000..204b108
--- /dev/null
+++ b/Semestr 2/racket/lista5/props.rkt	
@@ -0,0 +1,52 @@
+#lang racket
+
+(provide conj conj-left conj-right conj?
+         disj disj-left disj-right disj?
+         neg neg-subf neg?
+         var?)
+
+
+(define (conj p q)
+  (list 'conj p q))
+
+(define (conj-left f)
+  (second f))
+
+(define (conj-right f)
+  (third f))
+
+(define (conj? t)
+  (and (list? t)
+        (= 3 (length t))
+        (eq? 'conj (car t))))
+
+
+(define (disj p q)
+  (list 'disj p q))
+
+(define (disj-left f)
+  (second f))
+
+(define (disj-right f)
+  (third f))
+
+(define (disj? t)
+  (and (list? t)
+        (= 3 (length t))
+        (eq? 'disj (car t))))
+
+
+(define (neg x)
+  (list 'neg x))
+
+(define (neg-subf x)
+  (second x))
+
+(define (neg? t)
+  (and (list? t)
+        (= 2 (length t))
+        (eq? 'neg (car t))))
+
+
+(define (var? t)
+  (symbol? t))
diff --git a/Semestr 2/racket/lista5/skrr/solution.bak b/Semestr 2/racket/lista5/skrr/solution.bak
new file mode 100644
index 0000000..72c7f36
--- /dev/null
+++ b/Semestr 2/racket/lista5/skrr/solution.bak	
@@ -0,0 +1,135 @@
+#lang racket
+
+(provide falsifiable-cnf?)
+(require "props.rkt")
+
+(define (prop? f)
+  (or (var? f)
+      (and (neg? f)
+           (prop? (neg-subf f)))
+      (and (disj? f)
+           (prop? (disj-left f))
+           (prop? (disj-right f)))
+      (and (conj? f)
+           (prop? (conj-left f))
+           (prop? (conj-right f)))))
+
+(define (lit-var f)
+  (cond [(var? f) f]
+        [(neg? f) (neg-subf f)]
+        [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)]))
+      
+(define (free-vars f)
+  (cond [(null? f) null]
+        [(var? f) (list f)]
+        [(neg? f) (free-vars (neg-subf f))]
+        [(conj? f) (append (free-vars (conj-left f))
+                           (free-vars (conj-right f)))]
+        [(disj? f) (append (free-vars (disj-left f))
+                           (free-vars (disj-right f)))]
+        [else (error "Zła formula -- FREE-VARS" f)]))
+
+(define (gen-vals xs)
+  (if (null? xs)
+      (list null)
+      (let*
+          ((vss (gen-vals (cdr xs)))
+           (x (car xs))
+           (vst (map (λ (vs) (cons (list x true) vs)) vss))
+           (vsf (map (λ (vs) (cons (list x false) vs)) vss)))
+        (append vst vsf))))
+
+(define (eval-formula f evaluation)
+  (cond [(var? f)
+         (let ((val (assoc f evaluation)))
+           (if (not val)
+               (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation)
+               (cadr val)))]
+        [(neg? f) (not (eval-formula (neg-subf f) evaluation))]
+        [(disj? f) (or (eval-formula (disj-left f) evaluation)
+                       (eval-formula (disj-right f) evaluation))]
+        [(conj? f) (and (eval-formula (conj-left f) evaluation)
+                        (eval-formula (conj-right f) evaluation))]
+        [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)]))
+
+(define (falsifiable-eval? f)
+  (let* ((evaluations (gen-vals (free-vars f)))
+         (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations)))
+    (ormap false? results)))
+
+(define (nff? f)
+  (cond [(lit? f) true]
+        [(neg? f) false]
+        [(conj? f) (and (nff? (conj-left f))
+                        (nff? (conj-right f)))]
+        [(disj? f) (and (nff? (disj-left f))
+                        (nff? (disj-right f)))]
+        [else (error "Zła formuła -- NFF?" f)]))
+
+(define (convert-to-nnf f)
+  (cond [(lit? f) f]
+        [(neg? f) (convert-negation (neg-subf f))]
+        [(conj? f) (conj (convert-to-nnf (conj-left f))
+                              (convert-to-nnf (conj-right f)))]
+        [(disj? f) (disj (convert-to-nnf (disj-left f))
+                              (convert-to-nnf (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT" f)]))
+
+(define (convert-negation f)
+  (cond [(lit? f)
+         (if (var? f)
+             (neg f)
+             (neg-subf f))]
+        [(neg? f) (convert-to-nnf (neg-subf f))]
+        [(conj? f) (disj (convert-negation (conj-left f))
+                              (convert-negation (conj-right f)))]
+        [(disj? f) (conj (convert-negation (disj-left f))
+                              (convert-negation (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT-NEGATION" f)]))
+
+(define (clause? x)
+  (and (list? x)
+       (andmap lit? x)))
+
+(define (clause-empty? x)
+  (and (clause? x)
+       (null? x)))
+
+(define (cnf? x)
+  (and (list? x)
+       (andmap clause? x)))
+
+(define (flatmap proc seq)
+  (foldl append null (map proc seq)))
+
+(define (convert-to-cnf f)
+  (define (convert f)
+    (cond [(lit? f) (list (list f))]
+          [(conj? f) (append (convert-to-cnf (conj-left f))
+                             (convert-to-cnf (conj-right f)))]
+          [(disj? f)
+           (let ((clause-left (convert-to-cnf (disj-left f)))
+                 (clause-right (convert-to-cnf (disj-right f))))
+             (flatmap (λ (clause)
+                        (map (λ (clause2)
+                               (append clause2 clause)) clause-left))
+                      clause-right))]))
+  (convert (convert-to-nnf f)))
+
+(define (falsifiable-clause? clause)
+  (cond [(clause-empty? clause) true]
+        [(lit? (findf (λ (l) (equal?
+                              l
+                              (convert-to-nnf (neg (car clause)))))
+                              clause)) false]
+        [else (falsifiable-clause? (cdr clause))]))
+
+(define (falsifiable-cnf? f)
+  (define (neg-value lit)
+    (if (var? lit)
+        (list lit false)
+        (list (neg-subf lit) true)))
+  (ormap (λ (clause) (if (falsifiable-clause? clause)
+                         (map neg-value clause)
+                         false))
+         (convert-to-cnf f)))
\ No newline at end of file
diff --git a/Semestr 2/racket/lista5/skrr/solution.rkt b/Semestr 2/racket/lista5/skrr/solution.rkt
new file mode 100644
index 0000000..e8efbc9
--- /dev/null
+++ b/Semestr 2/racket/lista5/skrr/solution.rkt	
@@ -0,0 +1,88 @@
+#lang racket
+
+(require "props.rkt")
+(provide falsifiable-cnf?)
+
+(define (lit? f)
+  (or (var? f)
+      (and (neg? f)
+           (var? (neg-subf f)))))
+
+(define (lit-pos v)
+  v)
+
+(define (lit-neg v)
+  (neg v))
+
+(define (lit-var l)
+  (if (var? l)
+      l
+      (neg-subf l)))
+
+(define (lit-pos? l)
+  (var? l))
+
+(define (to-nnf f)
+  (cond
+   [(var? f)  (lit-pos f)]
+   [(neg? f)  (to-nnf-neg (neg-subf f))]
+   [(conj? f) (conj (to-nnf (conj-left f))
+                    (to-nnf (conj-right f)))]
+   [(disj? f) (disj (to-nnf (disj-left f))
+                    (to-nnf (disj-right f)))]))
+
+(define (to-nnf-neg f)
+  (cond
+   [(var? f)  (lit-neg f)]
+   [(neg? f)  (to-nnf (neg-subf f))]
+   [(conj? f) (disj (to-nnf-neg (conj-left f))
+                    (to-nnf-neg (conj-right f)))]
+   [(disj? f) (conj (to-nnf-neg (disj-left f))
+                    (to-nnf-neg (disj-right f)))]))
+
+(define (mk-cnf xss)
+  (cons 'cnf xss))
+
+(define (clause? f)
+  (and (list? f)
+       (andmap lit? f)))
+
+(define (cnf? f)
+  (and (pair? f)
+       (eq? 'cnf (car f))
+       (list? (cdr f))
+       (andmap clause? (cdr f))))
+
+(define (to-cnf f)
+  (define (join xss yss)
+    (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss)))
+  (define (go f)
+    (cond
+     [(lit? f)  (list (list f))]
+     [(conj? f) (append (go (conj-left f))
+                        (go (conj-right f)))]
+     [(disj? f) (join (go (disj-left f))
+                      (go (disj-right f)))]))
+  (mk-cnf (go f)))
+
+(define (clause-empty? x)
+  (and (clause? x)
+       (null? x)))
+
+(define (falsifiable-clause? clause)
+  (cond [(clause-empty? clause) true]
+        [(lit? (findf (λ (l) (equal?
+                              l
+                              (to-nnf (neg (car clause)))))
+                              clause)) false]
+        [else (falsifiable-clause? (cdr clause))]))
+
+(define (falsifiable-cnf? f)
+  (define (neg-value lit)
+    (if (var? lit)
+        (list lit false)
+        (list (neg-subf lit) true)))
+  (ormap (λ (clause) (if (falsifiable-clause? clause)
+                         (map neg-value clause)
+                         false))
+         (convert-to-cnf f)))
\ No newline at end of file
diff --git a/Semestr 2/racket/lista5/sol2.rkt b/Semestr 2/racket/lista5/sol2.rkt
new file mode 100644
index 0000000..d037472
--- /dev/null
+++ b/Semestr 2/racket/lista5/sol2.rkt	
@@ -0,0 +1,90 @@
+#lang racket
+(provide falsifiable-cnf?) (require "props.rkt")
+
+
+(define (falsifiable-cnf? p)
+  ;literał
+  (define (lit? p)
+    (or (var? p)
+        (and (neg? p) (var? (neg-subf p)))
+        ))
+  
+  (define (lit-pos? p)
+    (if (lit? p)
+        (var? p)
+        (error "not a literal" p)
+        ))
+  
+  (define (lit-var p)
+    (cond
+      [(not (lit? p)) (error "not a literal" p)]
+      [(lit-pos? p) p]
+      [else (neg-subf p)]
+      ))
+
+  (define (contr p)
+    (if (lit? p)
+        (if (neg? p) (neg-subf p) (neg p))
+        (error "not a literal" p)
+    ))
+
+  ;konwertowanie
+  (define (convert-to-cnf p)
+    (define (convert-to-nnf p)
+      (cond
+        [(lit? p) p]
+        [(and (neg? p) (conj? (neg-subf p)))
+         (let ((A (neg-subf p)))
+           (disj (convert-to-nnf (neg (conj-left A))) (convert-to-nnf (neg (conj-right A)))))]
+        [(and (neg? p) (disj? (neg-subf p)))
+         (let ((A (neg-subf p)))
+           (conj (convert-to-nnf (neg (disj-left A))) (convert-to-nnf (neg (disj-right A)))))]
+        [(and (neg? p) (neg? (neg-subf p))) (convert-to-nnf (neg-subf (neg-subf p)))]
+        [(conj? p) (conj (convert-to-nnf (conj-right p)) (convert-to-nnf (conj-left p)))]
+        [(disj? p) (disj (convert-to-nnf (disj-right p)) (convert-to-nnf (disj-left p)))]
+        [else (error "not a proposition" p)]))
+    
+    (define (flatmap proc seq)
+      (foldr append null (map proc seq)))
+    
+    (define (merge a b)
+      (flatmap (lambda (c) (map (lambda (c2) (append c c2)) b)) a))
+    
+    (define (convert p)
+      (cond
+        [(lit? p) (list (list p))]
+        [(conj? p) (append (convert (conj-left p)) (convert (conj-right p)))]
+        [(disj? p) (let* ((L (convert (disj-left p))) (R (convert (disj-right p))))
+                     (merge L R))]
+        [else (error "it should never be here" p)]
+        ))
+    
+    (map (lambda (c) (remove-duplicates c)) (convert (convert-to-nnf p))))
+
+  ;prawdziwa funkcja
+  (define cnf (convert-to-cnf p))
+  
+  (define (falsifiable-clause? c)
+    (cond
+      [(null? c) #t]
+      [(eq? #f (member (contr (car c)) c)) (falsifiable-clause? (cdr c))]
+      [else #f]
+    ))
+  
+  (define (falsified-clause c)
+    (if (null? c)
+        null
+        (cons (list (lit-var (car c)) (not (lit-pos? (car c)))) (falsified-clause (cdr c)))
+    ))
+  
+  (define (falsified-val p)
+    (cond
+      [(null? p)  false]
+      [(falsifiable-clause? (car p)) (falsified-clause (car p))]
+      [else (falsified-val (cdr p))]
+    )
+  )
+  (falsified-val cnf))
+
+
+;złożoność wykładnicza tak jak falsible-eval ale często w praktyce szybsza jak nie ma za dużo alternatyw.
\ No newline at end of file
diff --git a/Semestr 2/racket/lista5/solution.bak b/Semestr 2/racket/lista5/solution.bak
new file mode 100644
index 0000000..72c7f36
--- /dev/null
+++ b/Semestr 2/racket/lista5/solution.bak	
@@ -0,0 +1,135 @@
+#lang racket
+
+(provide falsifiable-cnf?)
+(require "props.rkt")
+
+(define (prop? f)
+  (or (var? f)
+      (and (neg? f)
+           (prop? (neg-subf f)))
+      (and (disj? f)
+           (prop? (disj-left f))
+           (prop? (disj-right f)))
+      (and (conj? f)
+           (prop? (conj-left f))
+           (prop? (conj-right f)))))
+
+(define (lit-var f)
+  (cond [(var? f) f]
+        [(neg? f) (neg-subf f)]
+        [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)]))
+      
+(define (free-vars f)
+  (cond [(null? f) null]
+        [(var? f) (list f)]
+        [(neg? f) (free-vars (neg-subf f))]
+        [(conj? f) (append (free-vars (conj-left f))
+                           (free-vars (conj-right f)))]
+        [(disj? f) (append (free-vars (disj-left f))
+                           (free-vars (disj-right f)))]
+        [else (error "Zła formula -- FREE-VARS" f)]))
+
+(define (gen-vals xs)
+  (if (null? xs)
+      (list null)
+      (let*
+          ((vss (gen-vals (cdr xs)))
+           (x (car xs))
+           (vst (map (λ (vs) (cons (list x true) vs)) vss))
+           (vsf (map (λ (vs) (cons (list x false) vs)) vss)))
+        (append vst vsf))))
+
+(define (eval-formula f evaluation)
+  (cond [(var? f)
+         (let ((val (assoc f evaluation)))
+           (if (not val)
+               (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation)
+               (cadr val)))]
+        [(neg? f) (not (eval-formula (neg-subf f) evaluation))]
+        [(disj? f) (or (eval-formula (disj-left f) evaluation)
+                       (eval-formula (disj-right f) evaluation))]
+        [(conj? f) (and (eval-formula (conj-left f) evaluation)
+                        (eval-formula (conj-right f) evaluation))]
+        [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)]))
+
+(define (falsifiable-eval? f)
+  (let* ((evaluations (gen-vals (free-vars f)))
+         (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations)))
+    (ormap false? results)))
+
+(define (nff? f)
+  (cond [(lit? f) true]
+        [(neg? f) false]
+        [(conj? f) (and (nff? (conj-left f))
+                        (nff? (conj-right f)))]
+        [(disj? f) (and (nff? (disj-left f))
+                        (nff? (disj-right f)))]
+        [else (error "Zła formuła -- NFF?" f)]))
+
+(define (convert-to-nnf f)
+  (cond [(lit? f) f]
+        [(neg? f) (convert-negation (neg-subf f))]
+        [(conj? f) (conj (convert-to-nnf (conj-left f))
+                              (convert-to-nnf (conj-right f)))]
+        [(disj? f) (disj (convert-to-nnf (disj-left f))
+                              (convert-to-nnf (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT" f)]))
+
+(define (convert-negation f)
+  (cond [(lit? f)
+         (if (var? f)
+             (neg f)
+             (neg-subf f))]
+        [(neg? f) (convert-to-nnf (neg-subf f))]
+        [(conj? f) (disj (convert-negation (conj-left f))
+                              (convert-negation (conj-right f)))]
+        [(disj? f) (conj (convert-negation (disj-left f))
+                              (convert-negation (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT-NEGATION" f)]))
+
+(define (clause? x)
+  (and (list? x)
+       (andmap lit? x)))
+
+(define (clause-empty? x)
+  (and (clause? x)
+       (null? x)))
+
+(define (cnf? x)
+  (and (list? x)
+       (andmap clause? x)))
+
+(define (flatmap proc seq)
+  (foldl append null (map proc seq)))
+
+(define (convert-to-cnf f)
+  (define (convert f)
+    (cond [(lit? f) (list (list f))]
+          [(conj? f) (append (convert-to-cnf (conj-left f))
+                             (convert-to-cnf (conj-right f)))]
+          [(disj? f)
+           (let ((clause-left (convert-to-cnf (disj-left f)))
+                 (clause-right (convert-to-cnf (disj-right f))))
+             (flatmap (λ (clause)
+                        (map (λ (clause2)
+                               (append clause2 clause)) clause-left))
+                      clause-right))]))
+  (convert (convert-to-nnf f)))
+
+(define (falsifiable-clause? clause)
+  (cond [(clause-empty? clause) true]
+        [(lit? (findf (λ (l) (equal?
+                              l
+                              (convert-to-nnf (neg (car clause)))))
+                              clause)) false]
+        [else (falsifiable-clause? (cdr clause))]))
+
+(define (falsifiable-cnf? f)
+  (define (neg-value lit)
+    (if (var? lit)
+        (list lit false)
+        (list (neg-subf lit) true)))
+  (ormap (λ (clause) (if (falsifiable-clause? clause)
+                         (map neg-value clause)
+                         false))
+         (convert-to-cnf f)))
\ No newline at end of file
diff --git a/Semestr 2/racket/lista5/solution.rkt b/Semestr 2/racket/lista5/solution.rkt
new file mode 100644
index 0000000..67964d8
--- /dev/null
+++ b/Semestr 2/racket/lista5/solution.rkt	
@@ -0,0 +1,140 @@
+#lang racket
+
+(provide falsifiable-cnf?)
+(require "props.rkt")
+
+(define (prop? f)
+  (or (var? f)
+      (and (neg? f)
+           (prop? (neg-subf f)))
+      (and (disj? f)
+           (prop? (disj-left f))
+           (prop? (disj-right f)))
+      (and (conj? f)
+           (prop? (conj-left f))
+           (prop? (conj-right f)))))
+
+(define (lit? t)
+  (or (var? t)
+      (and (neg? t)
+           (var? (neg-subf t)))))
+
+(define (lit-var f)
+  (cond [(var? f) f]
+        [(neg? f) (neg-subf f)]
+        [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)]))
+      
+(define (free-vars f)
+  (cond [(null? f) null]
+        [(var? f) (list f)]
+        [(neg? f) (free-vars (neg-subf f))]
+        [(conj? f) (append (free-vars (conj-left f))
+                           (free-vars (conj-right f)))]
+        [(disj? f) (append (free-vars (disj-left f))
+                           (free-vars (disj-right f)))]
+        [else (error "Zła formula -- FREE-VARS" f)]))
+
+(define (gen-vals xs)
+  (if (null? xs)
+      (list null)
+      (let*
+          ((vss (gen-vals (cdr xs)))
+           (x (car xs))
+           (vst (map (λ (vs) (cons (list x true) vs)) vss))
+           (vsf (map (λ (vs) (cons (list x false) vs)) vss)))
+        (append vst vsf))))
+
+(define (eval-formula f evaluation)
+  (cond [(var? f)
+         (let ((val (assoc f evaluation)))
+           (if (not val)
+               (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation)
+               (cadr val)))]
+        [(neg? f) (not (eval-formula (neg-subf f) evaluation))]
+        [(disj? f) (or (eval-formula (disj-left f) evaluation)
+                       (eval-formula (disj-right f) evaluation))]
+        [(conj? f) (and (eval-formula (conj-left f) evaluation)
+                        (eval-formula (conj-right f) evaluation))]
+        [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)]))
+
+(define (falsifiable-eval? f)
+  (let* ((evaluations (gen-vals (free-vars f)))
+         (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations)))
+    (ormap false? results)))
+
+(define (nff? f)
+  (cond [(lit? f) true]
+        [(neg? f) false]
+        [(conj? f) (and (nff? (conj-left f))
+                        (nff? (conj-right f)))]
+        [(disj? f) (and (nff? (disj-left f))
+                        (nff? (disj-right f)))]
+        [else (error "Zła formuła -- NFF?" f)]))
+
+(define (convert-to-nnf f)
+  (cond [(lit? f) f]
+        [(neg? f) (convert-negation (neg-subf f))]
+        [(conj? f) (conj (convert-to-nnf (conj-left f))
+                              (convert-to-nnf (conj-right f)))]
+        [(disj? f) (disj (convert-to-nnf (disj-left f))
+                              (convert-to-nnf (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT" f)]))
+
+(define (convert-negation f)
+  (cond [(lit? f)
+         (if (var? f)
+             (neg f)
+             (neg-subf f))]
+        [(neg? f) (convert-to-nnf (neg-subf f))]
+        [(conj? f) (disj (convert-negation (conj-left f))
+                              (convert-negation (conj-right f)))]
+        [(disj? f) (conj (convert-negation (disj-left f))
+                              (convert-negation (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT-NEGATION" f)]))
+
+(define (clause? x)
+  (and (list? x)
+       (andmap lit? x)))
+
+(define (clause-empty? x)
+  (and (clause? x)
+       (null? x)))
+
+(define (cnf? x)
+  (and (list? x)
+       (andmap clause? x)))
+
+(define (flatmap proc seq)
+  (foldl append null (map proc seq)))
+
+(define (convert-to-cnf f)
+  (define (convert f)
+    (cond [(lit? f) (list (list f))]
+          [(conj? f) (append (convert-to-cnf (conj-left f))
+                             (convert-to-cnf (conj-right f)))]
+          [(disj? f)
+           (let ((clause-left (convert-to-cnf (disj-left f)))
+                 (clause-right (convert-to-cnf (disj-right f))))
+             (flatmap (λ (clause)
+                        (map (λ (clause2)
+                               (append clause2 clause)) clause-left))
+                      clause-right))]))
+  (map (lambda (clause) (remove-duplicates clause)) (convert (convert-to-nnf f))))
+
+(define (falsifiable-clause? clause)
+  (cond [(clause-empty? clause) true]
+        [(lit? (findf (λ (l) (equal?
+                              l
+                              (convert-to-nnf (neg (car clause)))))
+                              clause)) false]
+        [else (falsifiable-clause? (cdr clause))]))
+
+(define (falsifiable-cnf? f)
+  (define (neg-value lit)
+    (if (var? lit)
+        (list lit false)
+        (list (neg-subf lit) true)))
+  (ormap (λ (clause) (if (falsifiable-clause? clause)
+                         (map neg-value clause)
+                         false))
+         (convert-to-cnf f)))
\ No newline at end of file
diff --git a/Semestr 2/racket/lista5/xd.bak b/Semestr 2/racket/lista5/xd.bak
new file mode 100644
index 0000000..d814e10
--- /dev/null
+++ b/Semestr 2/racket/lista5/xd.bak	
@@ -0,0 +1,4 @@
+#lang racket
+
+(require "solution.rkt")
+
diff --git a/Semestr 2/racket/lista5/xd.rkt b/Semestr 2/racket/lista5/xd.rkt
new file mode 100644
index 0000000..64ce78c
--- /dev/null
+++ b/Semestr 2/racket/lista5/xd.rkt	
@@ -0,0 +1,4 @@
+#lang racket
+
+(require "solution.rkt")
+(require "props.rkt")
-- 
cgit v1.2.3