(
and

true
(not false)

(and true true)
(not (and true false))
(not (and false true))
(not (and false false))

(and true true true)
(not (and true true false))
(not (and true false true))
(not (and true false false))
(not (and false true true))
(not (and false true false))
(not (and false false true))
(not (and false false false))

(and true true true true)
(not (and true true true false))
(not (and true true false true))
(not (and true true false false))
(not (and true false true true))
(not (and true false true false))
(not (and true false false true))
(not (and true false false false))
(not (and false true true true))
(not (and false true true false))
(not (and false true false true))
(not (and false true false false))
(not (and false false true true))
(not (and false false true false))
(not (and false false false true))
(not (and false false false false))

(and true true true true true)
(not (and false p q r s))
(not (and p false q r s))
(not (and p q false r s))
(not (and p q r false s))
(not (and p q r s false))

(and (or true p) (or q true) (not (or false false)))
(and (or true p q) (or r true s) (or t u true) (not (or false false false)))
(and (or true a b c) (or d true e f) (or g h true i) (or j k l true) (not (or false false false false)))
(and (or true a b c d) (or e true f g h) (or i j true k l) (or m n o true p) (or q r s t true))
(not (or false false false false false))

(and (=> false p) (=> true true) (not (=> true false)))
(and (<=> true true) (<=> false false) (not (<=> p (not p))))
(and (xor true false) (xor false true) (not (xor true true)) (not (xor false false)))

(and (<=> p p) (or q (not q)) (=> r r) (=> (and s t) s) (=> u (or u v)))
(and (=> p true) (<=> (or q false) q) (<=> (and r true) r) (<=> (=> true s) s))
(and (<=> (ite true p q) p) (<=> (ite false r s) s) (<=> (<=> true t) t) (<=> (<=> false u) (not u)))
(and (<=> (and p q) (and q p)) (<=> (or r s) (or s r)) (<=> (<=> t u) (<=> u t)))
(and (<=> (and (and p q) r) (and p (and q r))) (<=> (or (or s t) u) (or s (or t u))))
(and (<=> (and p p) p) (<=> (or q q) q) (<=> (and r (or r s)) r) (<=> (or t (and t u)) t))
(<=> (ite p q q) q)
(and (=> (and (=> p q) (=> q r)) (=> p r)) (=> (and (<=> s t) (<=> t u)) (<=> s u)))
(and (<=> (=> p q) (=> (not q) (not p))) (<=> (<=> r s) (<=> (not r) (not s))))
(and (<=> (and p (or q r)) (or (and p q) (and p r))) (<=> (or s (and t u)) (and (or s t) (or s u))))
(and (<=> (=> (or p q) r) (and (=> p r) (=> q r))) (<=> (=> s (or t u)) (or (=> s t) (=> s u))))
(and (<=> (=> (and p q) r) (or (=> p r) (=> q r))) (<=> (=> s (and t u)) (and (=> s t) (=> s u))))
(<=> (=> (and p q) r) (=> p (=> q r)))
(and (<=> (not (not p)) p) (<=> (not (and q r)) (or (not q) (not r))) (<=> (not (or s t)) (and (not s) (not t))))
(and (<=> (not (ite p q r)) (ite p (not q) (not r))) (<=> (not (<=> s t)) (<=> s (not t))))
(and (<=> (=> p q) (or (not p) q)) (<=> (ite r s t) (or (and r s) (and (not r) t))))
(and (<=> (ite p q r) (and (=> p q) (=> (not p) r))) (<=> (<=> s t) (or (and s t) (and (not s) (not t)))))
(<=> (<=> p q) (and (=> p q) (=> q p)))

(or (=> p q) (=> q p))
(or (not q) (not (and (=> p (not q)) p)))
(<=> (=> p (not q)) (not (and p q)))
(<=> (=> (or p q) r) (and (=> p r) (=> q r)))
(<=> (=> p (=> q r)) (=> (and p q) r))
(<=> (=> p (or q r)) (=> (and p (not q)) r))
(<=> (and p (=> q r)) (=> (or (not p) q) (and p r)))
(<=> (<=> p (<=> q r)) (<=> (<=> p q) r))
(<=> (ite p (and q r) (and (not q) s)) (ite q (and p r) (and (not p) s)))

(=> (and (ite P1 (or P2 P3) (or P3 P4))
            (ite P3 (not P6) (=> P4 P1))
            (not (and P2 P5)) (=> P2 P5))
       (not (=> P3 P6)))

)