+! Copyright (C) 2022 Alexander Ilin.
+! See http://factorcode.org/license.txt for BSD license.
+USING: boolean-expr literals tools.test ;
+IN: boolean-expr.tests
+
+${ P ¬ Q ⋀ } [ P ¬ P Q ⋁ ⋀ ] unit-test
+${ P ¬ Q ⋀ } [ P ¬ Q P ⋁ ⋀ ] unit-test
+${ P Q ⋀ } [ P P ¬ Q ⋁ ⋀ ] unit-test
+${ P Q ⋀ } [ P Q P ¬ ⋁ ⋀ ] unit-test
+
+! The following tests can't pass because only the distributivity of ∧ over ∨ is
+! implemented, but not the other way around, to prevent infinite loops.
+! ${ P ¬ Q ⋀ } [ P ¬ P Q ⋀ ⋁ ] unit-test
+! ${ Q P ¬ ⋀ } [ P ¬ Q P ⋀ ⋁ ] unit-test
+! ${ P Q ⋀ } [ P P ¬ Q ⋀ ⋁ ] unit-test
+! ${ P Q ⋀ } [ P Q P ¬ ⋀ ⋁ ] unit-test