(define (clause-set-map set clause-lit)
  (if (eq? (res-clause-neg clause-lit) '())
      (if (eq? set null) ;;pierwszy przypadek – gdy pojedynczy literał jest pozytywny
          null
          (let ([del-result (filter (lambda(x)
                           (eq? x (car (res-clause-pos clause-lit))))
                         (res-clause-pos (car set)))])
          (append
          (list (list 'res-clause
                 del-result
                 (res-clause-neg (car set))
                 (if (equal? (length del-result) (length (res-clause-pos (car set))))
                     (res-clause-proof (car set))
                     (res 'p (res-clause-proof clause-lit) (res-clause-proof (car set))))))
           (clause-set-map (cdr set) clause-lit))))

      (if (eq? set null) ;;gdy pojedynczy literał jest negatywny
          null
          (let ([del-result (filter (lambda(x)
                           (eq? x (car (res-clause-neg clause-lit))))
                         (res-clause-neg (car set)))])
          (append
           (list (list 'res-clause
                 (res-clause-pos (car set))
                 del-result
                 (if (equal? (length del-result) (length (res-clause-neg (car set))))
                     (res-clause-proof (car set))
                     (res 'p (res-clause-proof (car set)) (res-clause-proof clause-lit)))))
           (clause-set-map (cdr set) clause-lit))))))