(defun del_d (L)
(cond ((null L) nil)
((eq (car L) 'V) (del_d (cdr L)))
(T (cons (car L)(del_d (cdr L)))) ) )
(defun comb_not (L)
(cond ((null L) nil)
((eq (car L) '!) (cons (list '! (cadr L))(comb_not (cddr L))))
(T (cons (car L)(comb_not (cdr L)))) ) )
(defun comb_k (L)
(cond ((null L) nil)
((eq (cadr L) '&) (cond ((or (atom (car L))(member '! L)) (comb_k (cons (list (caddr L)(car L))(cdddr L))))
(T (comb_k (cons (cons (caddr L)(car L))(cdddr L)))) ) )
(T (cond ((atom (car L)) (cons (cons (car L)())(comb_k (cdr L))))
(T (cons (car L)(comb_k (cdr L)))) ) ) ) )
(defun mul1 (a L)
(cond ((member '! L) (cons (cons L a)()))
((null (cdr L)) (cons (cons (car L) a)()))
(T (append (cons (cons (car L)a)())(mul1 a (cdr L)))) ) )
(defun mul_1 (a L)
(cond ((and (not (atom a))(not (member '! a))) (mul1 a L))
((member '! L) (cons (list a L)()))
((null (cdr L)) (cons (list a (car L))()))
(T (append (cons (list a (car L))())(mul_1 a (cdr L)))) ) )
(defun mult_2 (L1 L2)
(cond ((null (cdr L1)) (mul_1 (car L1) L2))
(T (append (mul_1 (car L1)L2)(mult_2 (cdr L1)L2))) ) )
(defun mult_s (L)
(cond ((null (cddr L)) (mult_2 (car L)(cadr L)))
(T (mult_s (cons (mult_2 (car L)(cadr L))(cddr L)))) ) )
(defun makeset (L)
(cond ((null L) nil)
((member (car L) (cdr L)) (makeset (cdr L)))
(T (cons (car L) (makeset (cdr L))) ) ) )
(defun makeset_pr (L)
(cond ((null L) nil)
((member (car L) (cdr L)) T)
(T (makeset_pr (cdr L))) ) )
(defun flatten_f (S)
(cond ((null S) nil)
((atom S) (cons S ()))
(T (append (flatten_f (car S))(flatten_f(cdr S)))) ) )
(defun log_op_not (L)
(cond ((makeset_pr (flatten_f L)) nil)
(T L) ) )
(defun log_op (L)
(cond ((null L) nil)
(T (cons (log_op_not (makeset (car L)))(log_op (cdr L)))) ) )
(defun del_null (L)
(cond ((null L) nil)
((null (car L)) (del_null (cdr L)))
(T (cons (car L)(del_null (cdr L)))) ) )
(defun l2_l1_pr (L1 L2)
(cond ((null L2) T)
((makeset_pr (flatten_f (cons (car L2) L1))) (l2_l1_pr L1 (cdr L2)))
(T nil) ) )
(defun l2_l1_ost (L1 L2)
(cond ((null L2) nil)
((not (makeset_pr (flatten_f (cons (car L2) L1)))) (cond ((not(atom (car L2))) (cons (cadr L2) (l2_l1_ost L1 (cdr L2))))
(T (cons (car L2) (l2_l1_ost L1 (cdr L2)))) ) )
(T (l2_l1_ost L1 (cdr L2))) ) )
(defun part_l2_l1 (L1 L2)
(cond ((null L2) L1)
((not(l2_l1_ost L1 (car L2))) nil)
(T (part_l2_l1 L1 (cdr L2))) ) )
(defun l1_part_l2 (L1 L2)
(cond ((null L2) nil)
((not(l2_l1_ost (car L2) L1)) (l1_part_l2 L1 (cdr L2)))
(T (cons (car L2) (l1_part_l2 L1 (cdr L2))) ) ) )
(defun log_op_lst (L)
(cond ((null L) nil)
((null(part_l2_l1 (car L) (cdr L))) (log_op_lst (cdr L)))
(T (cons (car L) (log_op_lst (l1_part_l2 (car L) (cdr L)))) ) ) )
(defun ins_d (L)
(cond ((null L) nil)
((null (cdr L)) L)
((null (cddr L)) (cons (car L) (cons 'V (cdr L))) )
(T (cons (car L) (cons 'V (ins_d (cdr L)))) ) ) )
(defun ins_k (L)
(cond ((AND (null (car L)) (not(null (cdr L)))) (ins_k (cdr L)))
((null L) '(1))
((null (cdr L)) (cons (ins_d (car L)) nil))
(T (cons (ins_d (car L)) (cons '& (ins_k (cdr L))) ) ) ) )
(defun enter_d (L)
(del_null (log_op_lst (log_op (mult_s (comb_k (comb_not (del_d L)))))) ) )
(defun print_sok (L)
(ins_k (enter_d L) ))
(defun make_not (a L)
(cond ((null a) (cons L nil))
( T (list (cons a L) (cons (list '! a) L))) ) )
(defun make_s (L1 L2)
(cond ((null (cdr L2)) (make_not (car L2) L1))
((not (eq (car L2) '!)) (append (make_s (car (make_not (car L2) L1)) (cdr L2)) (make_s (cadr (make_not (car L2) L1)) (cdr L2))) )
(T (make_s L1 (cdr L2))) ) )
(defun make_sov (L L3)
(cond ((null L3) L)
((null L) nil)
((null (l2_l1_ost (car L) L3) ) (cons (car L) (make_sov (cdr L) L3)) )
(T (append (make_s (car L) (l2_l1_ost (car L) L3)) (make_sov (cdr L) L3))) ) )
(defun print_sov (L)
(ins_k (make_sov (enter_d L) (makeset (flatten_f (enter_d L))))) )
(print (print_sok '(A V B V ! B)))
(print (print_sov '(A V B V ! B)))
(print (print_sok '(A V B V C V B)))
(print (print_sov '(A V B V C V B)))
(print (print_sok '(A V B V ! C V ! A)))
(print (print_sov '(A V B V ! C V ! A)))
(print (print_sok '(A & B V B & ! C)))
(print (MAKE_SOV '((B) (A (! C)))))
(print (print_sov '(A & B V B & ! C)))
;(print (print_sok '(D & F V B & ! C & D & N F)))
;(print (print_sov '(D & F V B & ! C & D & N F)))
;(print (print_sok '(A & C V B & C D)))
;(print (print_sov '(A & C V B & C D)))