diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs
index 6a15801cb..429243736 100644
--- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs
+++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs
@@ -28,6 +28,9 @@ private static bool IsLogic(Entity a, Entity b, Entity c)
             Andf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 | any2),
             Orf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 & any2),
             Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True,
+            // The same law with the operands the other way round. `or` is commutative, so
+            // leaving this out made the answer depend on which side the negation was written.
+            Orf(var any1a, Notf(var any1)) when any1 == any1a && IsLogic(any1) => True,
             Orf(Notf(var any1), var any2) when IsLogic(any1, any2) => any1.Implies(any2),
             Andf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
             Orf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
diff --git a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs
index 14ca60cc1..eecfaac8e 100644
--- a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs
+++ b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs
@@ -434,5 +434,28 @@ public void ExpandKeepsTheValueOfAQuotientOfFactorials(string input, int at, dou
         [InlineData("(x + y + 1)! / (x + y)!")]
         public void ExpandCancelsAQuotientOfFactorialsRatherThanLeavingIt(string input)
             => Assert.DoesNotContain(input.ToEntity().Expand().Nodes, node => node is Entity.Factorialf);
+
+        // https://github.com/asc-community/AngouriMath/issues/876
+        // There was one excluded-middle rule and it matched the negation on the left operand
+        // only. `or` is commutative, so the same proposition had two answers depending on
+        // which side it was written: `not (x < 0) or (x < 0)` was True while
+        // `(x < 0) or not (x < 0)` was left as written. A bare variable hid it, because the
+        // boolean minimiser reduces those whichever way round they are — it takes a
+        // comparison, which the minimiser does not treat as an atom, to see it.
+        [Theory]
+        [InlineData("not (x < 0) or (x < 0)")]
+        [InlineData("(x < 0) or not (x < 0)")]
+        [InlineData("not (x > 0) or (x > 0)")]
+        [InlineData("(x > 0) or not (x > 0)")]
+        [InlineData("not (x <= 0) or (x <= 0)")]
+        [InlineData("(x <= 0) or not (x <= 0)")]
+        [InlineData("not (a = b) or (a = b)")]
+        [InlineData("(a = b) or not (a = b)")]
+        [InlineData("not (x in RR) or (x in RR)")]
+        [InlineData("(x in RR) or not (x in RR)")]
+        [InlineData("not p or p")]
+        [InlineData("p or not p")]
+        public void ExcludedMiddleHoldsWhicheverOperandCarriesTheNegation(string input)
+            => Assert.Equal(Entity.Boolean.True, input.ToEntity().Simplify());
     }
 }