diff --git a/src/Lib/Types/Emver.hs b/src/Lib/Types/Emver.hs
index 48346e3..af40644 100644
--- a/src/Lib/Types/Emver.hs
+++ b/src/Lib/Types/Emver.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RankNTypes #-}
 
 -- |
@@ -71,6 +72,7 @@ import Startlude (
     seq,
     show,
     snd,
+    toS,
     ($),
     ($>),
     (&&),
@@ -84,6 +86,7 @@ import Startlude (
 import Control.Monad.Fail (fail)
 import Data.Aeson (ToJSONKey)
 import Data.Attoparsec.Text qualified as Atto
+import Data.String.Interpolate.IsString (i)
 import Data.Text qualified as T
 import GHC.Base (Ord (..), error)
 import GHC.Read qualified as GHC (
@@ -225,6 +228,10 @@ data VersionRange
     deriving (Eq)
 
 
+instance IsString VersionRange where
+    fromString = either error id . Atto.parseOnly parseRange . toS
+
+
 instance NFData VersionRange where
     rnf (Conj a b) = rnf a `seq` rnf b
     rnf (Disj a b) = rnf a `seq` rnf b
@@ -254,180 +261,210 @@ reduce :: VersionRange -> VersionRange
 reduce Any = Any
 reduce None = None
 reduce vr@(Anchor _ _) = vr
--- conj units
-reduce (Conj Any vr) = vr
-reduce (Conj vr Any) = vr
--- conj annihilators
-reduce (Conj None _) = None
-reduce (Conj _ None) = None
--- disj annihilators
-reduce (Disj Any _) = Any
-reduce (Disj _ Any) = Any
--- disj units
-reduce (Disj None vr) = vr
-reduce (Disj vr None) = vr
--- primitive conjunction reduction
-reduce x@(Conj a@(Anchor op pt) b@(Anchor op' pt')) = case compare pt pt' of
-    -- conj commutes so we can make normalization order the points
-    GT -> reduce (Conj b a)
-    -- trivial cases where the points are identical
-    EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of
-        -- the theorems found here will elucidate what is going on
-        -- https://faculty.uml.edu/klevasseur/ads/s-laws-of-set-theory.html
-        -- conj idempodent law: these sets are identical
-        (_, True, True) -> a
-        -- conj complement law: these sets are opposites
-        (_, False, True) -> None
-        -- inequality incompatibility: these sets do not overlap
-        (True, True, False) -> None
-        -- conj absorption law (right): the right set is more specific
-        (False, True, False) -> b
-        -- conj absorption law (left): the left set is more specific
-        (True, False, False) -> a
-        -- all that is left is to intersect these sets. In every one of these cases the intersection can be expressed
-        -- as exactly the ordering that is not mentioned by the other two.
-        (False, False, False) -> Anchor (Right $ complement (primOrd op) (primOrd op')) pt
-    -- pattern reduction, throughout you will see the following notation (primarily for visualization purposes)
-    -- o: this means 'eq'
-    -- >: this means 'lt' or 'lte'
-    -- <: this means 'gt' or 'gte'
-    -- x: this means 'neq'
-    -- you may find this notation a bit odd, after all the less than and greater than signs seem backwards, you can see
-    -- it more clearly by viewing them as area dividers. the wide part of the angle represents this concept of 'faces'.
-    -- By this analogy, > faces left, < faces right, x faces both left and right, and o faces neither left nor right
-    -- it turns out that we only care about the inner two components: the right facing component of the lesser point,
-    -- and the left facing component of the greater point. Why is left as an exercise to the reader.
-    LT -> case (fr op, fl op') of
-        -- Annihilator patterns: oo, ><, o<, >o
-        (False, False) -> None
-        -- Left specific patterns: ox, o>, >x, >>
-        (False, True) -> a
-        -- Right specific patterns: xo, <o, x<, <<
-        (True, False) -> b
-        -- Irreducible patterns: <>, <x, x>, xx
-        (True, True) -> x
--- primitive disjunction reduction
-reduce x@(Disj a@(Anchor op pt) b@(Anchor op' pt')) = case compare pt pt' of
-    GT -> reduce (Disj b a)
-    EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of
-        -- idempotence
-        (_, True, True) -> a
-        -- complement
-        (_, False, True) -> Any
-        -- union these sets
-        (True, True, False) -> Anchor (Left $ complement (primOrd op) (primOrd op')) pt
-        -- disj absorption left: the left set is more general
-        (False, False, False) -> a
-        -- disj absorption right: the right set is more general
-        (True, False, False) -> b
-        -- inequality hypercompatibility: these sets are universal
-        (False, True, False) -> Any
-    LT -> case (fr op, fl op') of
-        -- Annihilator patterns: <>, <x, x>, xx
-        (True, True) -> Any
-        -- Left general patterns: x<, xo, <o, <<
-        (True, False) -> a
-        -- Right general patterns: >x, ox, o>, >>
-        (False, True) -> b
-        -- Irreducible patterns: >< >o o< oo
-        (False, False) -> x
-reduce (Conj x y) = case (reduce x, reduce y) of
+reduce orig@(Conj x y) = case (reduce x, reduce y) of
+    -- conj units
+    (Any, vr) -> reduce vr
+    (vr, Any) -> reduce vr
+    -- conj annihilators
+    (None, _) -> None
+    (_, None) -> None
+    -- primitive conjunction reduction
+    (a@(Anchor op pt), b@(Anchor op' pt')) -> case compare pt pt' of
+        -- conj commutes so we can make normalization order the points
+        GT -> reduce (Conj b a)
+        -- trivial cases where the points are identical
+        EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of
+            -- the theorems found here will elucidate what is going on
+            -- https://faculty.uml.edu/klevasseur/ads/s-laws-of-set-theory.html
+            -- conj idempodent law: these sets are identical
+            (_, True, True) -> a
+            -- conj complement law: these sets are opposites
+            (_, False, True) -> None
+            -- inequality incompatibility: these sets do not overlap
+            (True, True, False) -> None
+            -- conj absorption law (left): the left set is more specific
+            (True, False, False) -> a
+            -- conj absorption law (right): the right set is more specific
+            (False, False, False) -> b
+            -- all that is left is to intersect these sets. In every one of these cases the intersection can be expressed
+            -- as exactly the ordering that is not mentioned by the other two.
+            (False, True, False) -> Anchor (Right $ complement (primOrd op) (primOrd op')) pt
+        -- pattern reduction, throughout you will see the following notation (primarily for visualization purposes)
+        -- o: this means 'eq'
+        -- >: this means 'lt' or 'lte'
+        -- <: this means 'gt' or 'gte'
+        -- x: this means 'neq'
+        -- you may find this notation a bit odd, after all the less than and greater than signs seem backwards, you can see
+        -- it more clearly by viewing them as area dividers. the wide part of the angle represents this concept of 'faces'.
+        -- By this analogy, > faces left, < faces right, x faces both left and right, and o faces neither left nor right
+        -- it turns out that we only care about the inner two components: the right facing component of the lesser point,
+        -- and the left facing component of the greater point. Why is left as an exercise to the reader.
+        LT -> case (fr op, fl op') of
+            -- Annihilator patterns: oo, ><, o<, >o
+            (False, False) -> None
+            -- Left specific patterns: ox, o>, >x, >>
+            (False, True) -> a
+            -- Right specific patterns: xo, <o, x<, <<
+            (True, False) -> b
+            -- Irreducible patterns: <>, <x, x>, xx
+            (True, True) -> orig
     (a@(Anchor opa pta), Conj b@(Anchor opb ptb) c@(Anchor opc ptc)) ->
         case (compare pta ptb, compare pta ptc) of
-            -- impossible because all anchors of equal versions reduce
-            (GT, GT) ->
-                -- here we are to the right of an irreducible conj
-                _
-            (LT, LT) ->
-                -- here we are to the left of an irreducible conj
-                _
-            (GT, LT) ->
-                -- here we are in the middle of an irreducible conj
-                _
             -- eq patterns reduce so prioritize conj'ing those
             (EQ, LT) -> conj (conj a b) c
             (GT, EQ) -> conj b (conj a c)
-            (_, GT) -> error "bug in anchor order normalization"
-            (LT, _) -> error "bug in anchor order normalization"
-            (EQ, EQ) -> error "bug in equal anchor version reduction"
-    _ -> _
--- left distribute
-reduce (Conj a (Disj p q)) = disj (conj a p) (conj a q)
--- right distribute
-reduce (Conj (Disj p q) b) = disj (conj b p) (conj b q)
-reduce x@(Conj a@(Conj _ _) b@(Anchor _ _)) = conj b a
-reduce x@(Conj a@(Anchor _ _) b@(Conj _ _)) = x
-reduce x@(Conj a@(Anchor op pt) b@(Conj p q)) = case (p, q) of
-    ((Anchor opP ptP), (Anchor opQ ptQ)) ->
-        if ptP >= ptQ
-            then bail
-            else case (opP, opQ) of
-                -- diamonds <>
-                (Right GT, Right LT) ->
-                    if
-                            | (op == lt || op == leq || op == eq) && pt <= ptP -> None
-                            | (op == gt || op == geq || op == neq) && pt <= ptP -> b
-                            | (op == lt || op == leq || op == neq) && pt >= ptQ -> b
-                            | (op == gt || op == geq || op == eq) && pt >= ptQ -> None
-                            | (op == lt || op == leq) -> Conj p a
-                            | (op == gt || op == geq) -> Conj a q
-                            | op == eq -> a
-                            | op == neq -> Conj b a
-                            | otherwise -> x
-                (Left LT, Right LT) ->
-                    if
-                            | (op == lt || op == leq || op == eq) && pt < ptP -> None
-                            | (op == gt || op == geq || op == neq) && pt < ptP -> b
-                            | op == lt && pt == ptP -> None
-                            | op == leq && pt == ptP -> Anchor (Right EQ) pt
-                            | op == eq && pt == ptP -> a
-                            | op == gt && pt == ptP -> Conj a q
-                            | op == geq && pt == ptP -> b
-                            | op == neq && pt == ptP -> Conj (Anchor (Right GT) pt) q
-                            | (op == geq || op == neq) && pt == ptP -> b
-                            | (op == lt || op == leq || op == neq) && pt >= ptQ -> b
-                            | (op == gt || op == geq || op == eq) && pt >= ptQ -> None
-                            | (op == lt || op == leq) -> Conj p a
-                            | (op == gt || op == geq) -> Conj a q
-                            | op == eq -> a
-                            | op == neq -> Conj b a
-                            | otherwise -> x
-                (Right GT, Left GT) ->
-                    if
-                            | (op == lt || op == leq || op == eq) && pt <= ptP -> None
-                            | (op == gt || op == geq || op == neq) && pt <= ptP -> b
-                            | (op == gt || op == geq || op == eq) && pt > ptQ -> None
-                            | (op == lt || op == leq || op == neq) && pt > ptQ -> b
-                            | op == lt && pt == ptQ -> Conj p a
-                            | op == leq && pt == ptQ -> b
-                            | op == eq && pt == ptQ -> a
-                            | op == gt && pt == ptQ -> None
-                            | op == geq && pt == ptQ -> Anchor (Right EQ) pt
-                            | op == neq && pt == ptQ -> Conj p (Anchor lt pt)
-                            | (op == gt || op == geq) -> Conj a q
-                            | (op == lt || op == leq) -> Conj p a
-                            | op == eq -> a
-                            | op == neq -> Conj b a
-                            | otherwise -> x
-                (Left LT, Left GT) ->
-                    if
-                            | (op == lt || op == leq || op == eq) && pt < ptP -> None
-                            | (op == gt || op == geq || op == neq) && pt < ptP -> b
-                            | otherwise -> x
-                -- fish left <x
-                (Right GT, Left EQ) -> x
-                (Left LT, Left EQ) -> x
-                -- fish right x>
-                (Left EQ, Right LT) -> x
-                (Left EQ, Left GT) -> x
-                -- dead eyes xx
-                (Left EQ, Left EQ) -> x
-                -- all other states are unstable for conj
-                _ -> bail
-    _ -> x
-    where
-        bail = reduce (Conj a (reduce b))
-reduce rest = rest
+            -- here we are to the right of an irreducible conj, so we try to reduce with the right side
+            (GT, GT) -> case conj c a of
+                -- cascade if successful
+                cca@(Anchor _ _) -> conj b cca
+                -- otherwise we move xs out right
+                -- we know for sure at this point that the opc is x
+                _ -> case (fl opb, fr opa) of
+                    (True, True) -> Conj b (Conj c a) -- xxx: x (xx)
+                    (True, False) -> Conj a (Conj b c) -- xx>: > (xx)
+                    (False, True) -> Conj b (Conj c a) -- <xx: < (xx)
+                    (False, False) -> Conj (Conj b a) c -- <x>: (<>) x
+                    -- here we are to the left of an irreducible conj, so we try to reduce the left side
+            (LT, LT) -> case conj a b of
+                -- cascade if successful
+                cab@(Anchor _ _) -> conj cab c
+                -- otherwise we move xs out right
+                -- we know for sure that opb is x
+                _ -> case (fl opa, fr opc) of
+                    (True, True) -> Conj a (Conj b c) -- xxx: x (xx)
+                    (True, False) -> Conj c (Conj a b) -- xx>: > (xx)
+                    (False, True) -> Conj a (Conj b c) -- <xx: < (xx)
+                    (False, False) -> Conj (Conj a c) b -- <x>: (<>) x
+                    -- here we are in the middle of an irreducible conj
+            (GT, LT)
+                -- <x> <xx xx> xxx all irreducible
+                | opa == neq -> conj b (conj a c)
+                -- if there is a remaining left face component it will reduce with the right side
+                | fl opa -> conj b (conj a c)
+                -- corollary
+                | fr opa -> conj (conj b a) c
+                -- only remaining case is eq, which subsumes both sides
+                | otherwise -> a
+            -- impossible because all anchors of equal versions reduce
+            (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|]
+            -- ordinarily we reorder things so the lesser point is on the left
+            -- the only exception to this is the accumulation of x's on the right
+            -- so these cases should be impossible
+            _
+                | opb == neq && opc == neq -> orig
+                | otherwise -> error $ [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|]
+    (x'@(Conj (Anchor _ _) (Anchor _ _)), y'@(Anchor _ _)) -> conj y' x'
+    -- distribute right
+    (x', Disj p q) -> disj (conj x' p) (conj x' q)
+    -- distribute left
+    (Disj p q, y') -> disj (conj p y') (conj q y')
+    -- insert anchor into accumulation tree
+    (a@(Anchor opa pta), Conj b@(Anchor opb ptb) at@(Conj atl atr)) -> error "TODO manage accumulation trees"
+    -- reconcile free anchor with essential anchors in accumulation tree
+    (a@(Anchor opa _), Conj (Conj b@(Anchor _ _) c@(Anchor _ _)) r) -> case (fl opa, fr opa) of
+        (True, True) -> Conj (Conj b c) (conj a r)
+        (True, False) -> Conj (Conj b (conj a c)) r
+        (False, True) -> Conj (Conj (conj b a) c) r
+        (False, False) -> a
+    (x'@(Conj (Conj _ _) (Anchor _ _)), y'@(Anchor _ _)) -> conj y' x'
+    (Conj a@(Anchor _ _) b@(Anchor _ _), y'@(Conj _ _)) -> conj a (conj b y')
+    (x', y') -> error [i|missing conj case: #{orig} -> #{x'}, #{y'}|]
+reduce orig@(Disj x y) = case (reduce x, reduce y) of
+    -- disj annihilators
+    (Any, _) -> Any
+    (_, Any) -> Any
+    -- disj units
+    (None, vr) -> reduce vr
+    (vr, None) -> reduce vr
+    -- primitive disj reduction
+    (a@(Anchor op pt), b@(Anchor op' pt')) -> case compare pt pt' of
+        GT -> reduce (Disj b a)
+        EQ -> case (isRight op, isRight op == isRight op', primOrd op == primOrd op') of
+            -- idempotence
+            (_, True, True) -> a
+            -- complement
+            (_, False, True) -> Any
+            -- union these sets
+            (True, True, False) -> Anchor (Left $ complement (primOrd op) (primOrd op')) pt
+            -- disj absorption left: the left set is more general
+            (False, False, False) -> a
+            -- disj absorption right: the right set is more general
+            (True, False, False) -> b
+            -- inequality hypercompatibility: these sets are universal
+            (False, True, False) -> Any
+        LT -> case (fr op, fl op') of
+            -- Annihilator patterns: <>, <x, x>, xx
+            (True, True) -> Any
+            -- Left general patterns: x<, xo, <o, <<
+            (True, False) -> a
+            -- Right general patterns: >x, ox, o>, >>
+            (False, True) -> b
+            -- Irreducible patterns: >< >o o< oo
+            (False, False) -> x
+    (a@(Anchor opa pta), Disj b@(Anchor opb ptb) c@(Anchor opc ptc)) -> case (compare pta ptb, compare pta ptc) of
+        -- eq patterns reduce so prioritize disj'ing those
+        (EQ, LT) -> disj (disj a b) c
+        (GT, EQ) -> disj b (disj a c)
+        -- here we are to the right of an irreducible conj, so we try to reduce with the right side
+        (GT, GT) -> case disj c a of
+            -- cascade if successful
+            dca@(Anchor _ _) -> disj b dca
+            -- otherwise we move o's out right
+            -- we know for sure at this point that the opc is o
+            _ -> case (fl opb, fr opa) of
+                (True, True) -> Disj (Disj b a) c -- >o<: (><) o
+                (True, False) -> Disj b (Disj c a) -- >oo: > (oo)
+                (False, True) -> Disj a (Disj b c) -- oo<: < (oo)
+                (False, False) -> Disj b (Disj c a) -- ooo: o (oo)
+                -- here we are to the left of an irreducible conj, so we try to reduce the left side
+        (LT, LT) -> case disj a b of
+            --     -- cascade if successful
+            dab@(Anchor _ _) -> disj dab c
+            -- otherwise we move xs out right
+            -- we know for sure that opb is o
+            _ -> case (fl opa, fr opc) of
+                (True, True) -> Disj (Disj a c) b -- >o<: (><) o
+                (True, False) -> Disj a (Disj b c) -- >oo: > (oo)
+                (False, True) -> Disj c (Disj a b) -- oo<: < (oo)
+                (False, False) -> Disj a (Disj b c) -- ooo: o (oo)
+                -- here we are in the middle of an irreducible conj
+        (GT, LT)
+            -- >o< >oo oo< ooo all irreducible
+            | opa == eq -> disj b (disj a c)
+            -- if there is a remaining left face component it will reduce with the left side
+            | fl opa -> disj (disj b a) c
+            -- corollary
+            | fr opa -> disj b (disj a c)
+            -- only remaining case is neq, which subsumes both sides
+            | otherwise -> a
+        -- impossible because all anchors of equal versions reduce
+        (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|]
+        -- ordinarily we reorder things so the lesser point is on the left
+        -- the only exception to this is the accumulation of x's on the right
+        -- so these cases should be impossible
+        _
+            | opb == eq && opc == eq -> orig
+            | otherwise -> error $ [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|]
+    (x'@(Disj (Anchor _ _) (Anchor _ _)), y'@(Anchor _ _)) -> disj y' x'
+    (a@(Anchor opa pta), y'@(Conj b@(Anchor opb ptb) c@(Anchor opc ptc))) ->
+        case (compare pta ptb, compare pta ptc) of
+            (GT, GT) -> if fl opa then a else Disj y' a
+            (LT, LT) -> if fr opa then a else Disj a y'
+            (GT, LT) -> case (fl opa, fr opa) of
+                (True, True) -> Any
+                (True, False) -> c
+                (False, True) -> b
+                (False, False) -> y'
+            (EQ, EQ) -> error [i|bug in equal anchor version reduction: #{orig} -> #{a}, #{b}, #{c}|]
+            (EQ, _) -> error "TODO1"
+            (_, EQ) -> error "TODO2"
+            (LT, GT) -> error [i|bug in anchor order normalization: #{orig} -> #{a}, #{b}, #{c}|]
+    (x'@(Conj _ _), y'@(Anchor _ _)) -> disj y' x'
+    (Conj _ _, Conj _ _) -> error "Disj (Conj _ _) (Conj _ _)"
+    (Conj _ _, _) -> error "Disj (Conj _ _) _"
+    (_, Conj _ _) -> error "Disj _ (Conj _ _)"
+    (Disj _ _, Disj _ _) -> error "Disj (Disj _ _) (Disj _ _)"
+    (x', y') -> error [i|missing disj case: #{orig} -> #{x'}, #{y'}|]
 
 
 exactly :: Version -> VersionRange
@@ -460,14 +497,14 @@ paren = mappend "(" . flip mappend ")"
 
 newtype AnyRange = AnyRange {unAnyRange :: VersionRange}
 instance Semigroup AnyRange where
-    (<>) = AnyRange <<$>> disj `on` unAnyRange
+    (<>) = AnyRange <<$>> Disj `on` unAnyRange
 instance Monoid AnyRange where
     mempty = AnyRange None
 
 
 newtype AllRange = AllRange {unAllRange :: VersionRange}
 instance Semigroup AllRange where
-    (<>) = AllRange <<$>> conj `on` unAllRange
+    (<>) = AllRange <<$>> Conj `on` unAllRange
 instance Monoid AllRange where
     mempty = AllRange Any
 
diff --git a/test/Lib/Types/EmverProp.hs b/test/Lib/Types/EmverProp.hs
index 744ef63..b2b22d0 100644
--- a/test/Lib/Types/EmverProp.hs
+++ b/test/Lib/Types/EmverProp.hs
@@ -1,15 +1,19 @@
 {-# LANGUAGE TemplateHaskell #-}
+
 module Lib.Types.EmverProp where
 
-import           Startlude               hiding ( Any
-                                                , reduce
-                                                )
+import Startlude hiding (
+    Any,
+    reduce,
+ )
+
+import Data.Attoparsec.Text qualified as Atto
+import Hedgehog as Test
+import Hedgehog.Gen as Gen
+import Hedgehog.Range
+import Lib.Types.Emver
+import UnliftIO qualified
 
-import qualified Data.Attoparsec.Text          as Atto
-import           Hedgehog                      as Test
-import           Hedgehog.Gen                  as Gen
-import           Hedgehog.Range
-import           Lib.Types.Emver
 
 versionGen :: MonadGen m => m Version
 versionGen = do
@@ -19,118 +23,137 @@ versionGen = do
     d <- word (linear 0 30)
     pure $ Version (a, b, c, d)
 
+
 rangeGen :: MonadGen m => m VersionRange
 rangeGen = choice [pure None, pure Any, anchorGen, disjGen, conjGen]
 
+
 anchorGen :: MonadGen m => m VersionRange
 anchorGen = do
     c <- element [LT, EQ, GT]
     f <- element [Left, Right]
     Anchor (f c) <$> versionGen
 
+
 conjGen :: MonadGen m => m VersionRange
 conjGen = liftA2 Conj rangeGen rangeGen
 
+
 disjGen :: MonadGen m => m VersionRange
 disjGen = liftA2 Disj rangeGen rangeGen
 
+
 prop_conjAssoc :: Property
 prop_conjAssoc = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
-    c   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
+    c <- forAll rangeGen
     obs <- forAll versionGen
-    (obs <|| conj a (conj b c)) === (obs <|| conj (conj a b) c)
+    (obs <|| Conj a (Conj b c)) === (obs <|| Conj (Conj a b) c)
+
 
 prop_conjCommut :: Property
 prop_conjCommut = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
     obs <- forAll versionGen
-    (obs <|| conj a b) === (obs <|| conj b a)
+    (obs <|| Conj a b) === (obs <|| Conj b a)
+
 
 prop_disjAssoc :: Property
 prop_disjAssoc = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
-    c   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
+    c <- forAll rangeGen
     obs <- forAll versionGen
-    (obs <|| disj a (disj b c)) === (obs <|| disj (disj a b) c)
+    (obs <|| Disj a (Disj b c)) === (obs <|| Disj (Disj a b) c)
+
 
 prop_disjCommut :: Property
 prop_disjCommut = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
     obs <- forAll versionGen
-    (obs <|| disj a b) === (obs <|| disj b a)
+    (obs <|| Disj a b) === (obs <|| Disj b a)
+
 
 prop_anyIdentConj :: Property
 prop_anyIdentConj = property $ do
-    a   <- forAll rangeGen
+    a <- forAll rangeGen
     obs <- forAll versionGen
-    obs <|| conj Any a === obs <|| a
+    obs <|| Conj Any a === obs <|| a
+
 
 prop_noneIdentDisj :: Property
 prop_noneIdentDisj = property $ do
-    a   <- forAll rangeGen
+    a <- forAll rangeGen
     obs <- forAll versionGen
-    obs <|| disj None a === obs <|| a
+    obs <|| Disj None a === obs <|| a
+
 
 prop_noneAnnihilatesConj :: Property
 prop_noneAnnihilatesConj = property $ do
-    a   <- forAll rangeGen
+    a <- forAll rangeGen
     obs <- forAll versionGen
-    obs <|| conj None a === obs <|| None
+    obs <|| Conj None a === obs <|| None
+
 
 prop_anyAnnihilatesDisj :: Property
 prop_anyAnnihilatesDisj = property $ do
-    a   <- forAll rangeGen
+    a <- forAll rangeGen
     obs <- forAll versionGen
-    obs <|| disj Any a === obs <|| Any
+    obs <|| Disj Any a === obs <|| Any
+
 
 prop_conjDistributesOverDisj :: Property
 prop_conjDistributesOverDisj = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
-    c   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
+    c <- forAll rangeGen
     obs <- forAll versionGen
-    obs <|| conj a (disj b c) === obs <|| disj (conj a b) (conj a c)
+    obs <|| Conj a (Disj b c) === obs <|| Disj (Conj a b) (Conj a c)
+
 
 prop_disjDistributesOverConj :: Property
 prop_disjDistributesOverConj = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
-    c   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
+    c <- forAll rangeGen
     obs <- forAll versionGen
-    obs <|| disj a (conj b c) === obs <|| conj (disj a b) (disj a c)
+    obs <|| Disj a (Conj b c) === obs <|| Conj (Disj a b) (Disj a c)
+
 
 prop_anyAcceptsAny :: Property
 prop_anyAcceptsAny = property $ do
     obs <- forAll versionGen
     assert $ obs <|| Any
 
+
 prop_noneAcceptsNone :: Property
 prop_noneAcceptsNone = property $ do
     obs <- forAll versionGen
     assert . not $ obs <|| None
 
+
 prop_conjBoth :: Property
 prop_conjBoth = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
     obs <- forAll versionGen
-    (obs <|| conj a b) === (obs <|| a && obs <|| b)
+    (obs <|| Conj a b) === (obs <|| a && obs <|| b)
+
 
 prop_disjEither :: Property
 prop_disjEither = property $ do
-    a   <- forAll rangeGen
-    b   <- forAll rangeGen
+    a <- forAll rangeGen
+    b <- forAll rangeGen
     obs <- forAll versionGen
-    (obs <|| disj a b) === (obs <|| a || obs <|| b)
+    (obs <|| Disj a b) === (obs <|| a || obs <|| b)
+
 
 prop_rangeParseRoundTrip :: Property
 prop_rangeParseRoundTrip = withShrinks 0 . property $ do
-    a   <- forAll rangeGen
+    a <- forAll rangeGen
     obs <- forAll versionGen
     -- we do not use 'tripping' here since 'tripping' requires equality of representation
     -- we only want to check equality up to OBSERVATION
@@ -138,38 +161,44 @@ prop_rangeParseRoundTrip = withShrinks 0 . property $ do
     annotateShow (Atto.parseOnly parseRange (show a))
     (satisfies obs <$> Atto.parseOnly parseRange (show a)) === Right (satisfies obs a)
 
+
 prop_anchorLeftIsNegatedRight :: Property
 prop_anchorLeftIsNegatedRight = property $ do
-    a   <- forAll anchorGen
+    a <- forAll anchorGen
     neg <- case a of
         Anchor (Right o) v -> pure $ Anchor (Left o) v
-        Anchor (Left  o) v -> pure $ Anchor (Right o) v
-        _                  -> Test.discard
+        Anchor (Left o) v -> pure $ Anchor (Right o) v
+        _ -> Test.discard
     obs <- forAll versionGen
     obs <|| a /== obs <|| neg
 
+
 prop_reduceConjAnchor :: Property
 prop_reduceConjAnchor = property $ do
-    a   <- forAll anchorGen
-    b   <- forAll anchorGen
+    a <- forAll anchorGen
+    b <- forAll anchorGen
     obs <- forAll versionGen
-    obs <|| reduce (conj a b) === obs <|| conj a b
+    obs <|| reduce (Conj a b) === obs <|| Conj a b
+
 
 prop_reduceDisjAnchor :: Property
 prop_reduceDisjAnchor = property $ do
-    a   <- forAll anchorGen
-    b   <- forAll anchorGen
+    a <- forAll anchorGen
+    b <- forAll anchorGen
     obs <- forAll versionGen
-    obs <|| reduce (disj a b) === obs <|| disj a b
+    obs <|| reduce (Disj a b) === obs <|| Disj a b
+
 
 prop_reduceIdentity :: Property
-prop_reduceIdentity = withTests 1000 $ property $ do
-    -- a   <- forAll rangeGen
-    a   <- forAll conjGen
-    obs <- forAll versionGen
-    let b = reduce a
-    unless (b /= a) Test.discard
-    obs <|| a === obs <|| b
+prop_reduceIdentity = withTests 2000 . withDiscards 90 $
+    property $ do
+        -- a   <- forAll rangeGen
+        a <- forAll conjGen
+        obs <- forAll versionGen
+        b <- liftIO $ pure (reduce a) `catch` \e -> throwIO (e :: ErrorCall)
+        unless (b /= a) Test.discard
+        obs <|| a === obs <|| b
+
 
 tests :: IO Bool
 tests = checkParallel $ $$discover