diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,12 @@
 
 - ...
 
+## v0.3.0.0 (2025-01-01)
+
+- add `optimalOrder`
+- fix segfault on Apple M1 and ARM aarch64
+- minor improvements of documentation and tests
+
 ## v0.2.0.0 (2023-11-23)
 
 - rename `forall` (soon a keyword in GHC) to `forall_` and `exists` to `exists_`
diff --git a/HasCacBDD.cabal b/HasCacBDD.cabal
--- a/HasCacBDD.cabal
+++ b/HasCacBDD.cabal
@@ -1,5 +1,5 @@
 name:                HasCacBDD
-version:             0.2.0.0
+version:             0.3.0.0
 synopsis:            Haskell bindings for CacBDD
 homepage:            https://github.com/m4lvin/HasCacBDD
 license:             GPL-2
@@ -34,8 +34,8 @@
 
 custom-setup
   setup-depends:       base >= 4.8 && < 5,
-                       Cabal < 3.9,
-                       directory
+                       Cabal < 3.13,
+                       directory <1.4
 
 library
   exposed-modules:     Data.HasCacBDD,
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -3,8 +3,8 @@
 
 [![Release](https://img.shields.io/github/release/m4lvin/HasCacBDD.svg)](https://github.com/m4lvin/HasCacBDD/releases)
 [![Hackage](https://img.shields.io/hackage/v/HasCacBDD.svg)](https://hackage.haskell.org/package/HasCacBDD)
-[![GitLab CI](https://gitlab.com/m4lvin/HasCacBDD/badges/master/pipeline.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)
-[![Test Coverage](https://gitlab.com/m4lvin/HasCacBDD/badges/master/coverage.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/master/file/hpc/combined/all/hpc_index.html?job=test)
+[![GitLab CI](https://gitlab.com/m4lvin/HasCacBDD/badges/main/pipeline.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)
+[![Test Coverage](https://gitlab.com/m4lvin/HasCacBDD/badges/main/coverage.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/main/file/hpc/combined/all/hpc_index.html?job=test)
 
 Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management.
 
@@ -40,3 +40,5 @@
        Var 5 Bot Top
        λ> dis (neg (var 3)) (var 3)
        Top
+
+For further documentation, see <https://hackage.haskell.org/package/HasCacBDD/docs/Data-HasCacBDD.html>
diff --git a/c/BDDNodeC.cpp b/c/BDDNodeC.cpp
--- a/c/BDDNodeC.cpp
+++ b/c/BDDNodeC.cpp
@@ -7,21 +7,21 @@
 
 int BDD_Variable(BDD* this_ptr) { return this_ptr->Variable(); }
 
-BDD BDD_Then(const BDD* this_ptr) { return this_ptr->Then(); }
+void BDD_Then(BDD* ret_ptr, const BDD* this_ptr) { *ret_ptr = this_ptr->Then(); }
 
-BDD BDD_Else(const BDD* this_ptr) { return this_ptr->Else(); }
+void BDD_Else(BDD* ret_ptr, const BDD* this_ptr) { *ret_ptr = this_ptr->Else(); }
 
-BDD BDD_Exist(BDD* this_ptr, const BDD* cube) { return this_ptr->Exist(*cube); }
+void BDD_Exist(BDD* ret_ptr, BDD* this_ptr, const BDD* cube) { *ret_ptr = this_ptr->Exist(*cube); }
 
-BDD BDD_Universal(BDD* this_ptr, const BDD* cube) { return this_ptr->Universal(*cube); }
+void BDD_Universal(BDD* ret_ptr, BDD* this_ptr, const BDD* cube) { *ret_ptr = this_ptr->Universal(*cube); }
 
-BDD BDD_Restrict(const BDD* this_ptr, const BDD* other) { return this_ptr->Restrict(*other); }
+void BDD_Restrict(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = this_ptr->Restrict(*other); }
 
-BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other) { return this_ptr->Compose(v, *other); }
+void BDD_Compose(BDD* ret_ptr, const BDD* this_ptr, int v, const BDD* other) { *ret_ptr = this_ptr->Compose(v, *other); }
 
-BDD BDD_Permute(const BDD* this_ptr, const vector<int>* permu) { return this_ptr->Permute(*permu); }
+void BDD_Permute(BDD* ret_ptr, const BDD* this_ptr, const vector<int>* permu) { *ret_ptr = this_ptr->Permute(*permu); }
 
-BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube) { return this_ptr->AndExist(*other, *cube); }
+void BDD_AndExist(BDD* ret_ptr, BDD* this_ptr, const BDD* other, const BDD* cube) { *ret_ptr = this_ptr->AndExist(*other, *cube); }
 
 bool BDD_IsComp(BDD* this_ptr) { bool b = this_ptr->IsComp(); return b; }
 
@@ -29,32 +29,32 @@
 
 XBDDManager* XBDDManager_new(int varCount) { return new XBDDManager(varCount); }
 
-BDD XBDDManager_BddOne(XBDDManager* this_ptr) { return (BDD) this_ptr->BddOne(); }
+void XBDDManager_BddOne(BDD* ret_ptr, XBDDManager* this_ptr) { *ret_ptr = this_ptr->BddOne(); }
 
-BDD XBDDManager_BddZero(XBDDManager* this_ptr) { return (BDD) this_ptr->BddZero(); }
+void XBDDManager_BddZero(BDD* ret_ptr, XBDDManager* this_ptr) { *ret_ptr = this_ptr->BddZero(); }
 
-BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex) { BDD bar = this_ptr->BddVar(varIndex); return bar; }
+void XBDDManager_BddVar(BDD* ret_ptr, XBDDManager* this_ptr, int varIndex) { *ret_ptr = this_ptr->BddVar(varIndex); }
 
-BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { return (BDD) this_ptr->Ite(*f, *g, *h); }
+void XBDDManager_Ite(BDD* ret_ptr, XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { *ret_ptr = this_ptr->Ite(*f, *g, *h); }
 
 const XManager* XBDDManager_manager(const XBDDManager* this_ptr) { return this_ptr->manager(); }
 
-BDD BDD_Operator_Not(const BDD* this_ptr) { BDD bar = (! *this_ptr); return bar;  }
+void BDD_Operator_Not(BDD* ret_ptr, const BDD *this_ptr) { *ret_ptr = (!*this_ptr); }
 
 bool BDD_Operator_Equal(const BDD* this_ptr, const BDD* other) { bool b = (*this_ptr == *other); return b; }
 
-BDD BDD_Operator_Or(const BDD* this_ptr, const BDD* other) { BDD bar = (*this_ptr + *other); return bar; }
+void BDD_Operator_Or(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr + *other); }
 
-BDD BDD_Operator_And(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr * *other); }
+void BDD_Operator_And(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr * *other); }
 
-BDD BDD_Operator_Xor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr ^ *other); }
+void BDD_Operator_Xor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr ^ *other); }
 
-BDD BDD_Operator_LessEqual(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr <= *other); }
+void BDD_Operator_LessEqual(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr <= *other); }
 
-BDD BDD_Operator_Nor(const BDD* this_ptr, const BDD* other) { return (BDD) (*this_ptr % *other); }
+void BDD_Operator_Nor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr % *other); }
 
-BDD BDD_Operator_Nand(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr | *other); }
+void BDD_Operator_Nand(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr | *other); }
 
-BDD BDD_Operator_XNor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr & *other); }
+void BDD_Operator_XNor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr & *other); }
 
-void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime) { return this_ptr->ShowInfo(); }
+void XBDDManager_ShowInfo(XBDDManager* this_ptr) { this_ptr->ShowInfo(); }
diff --git a/c/BDDNodeC.h b/c/BDDNodeC.h
--- a/c/BDDNodeC.h
+++ b/c/BDDNodeC.h
@@ -5,35 +5,37 @@
 BDD* BDD_new();
 const XManager* BDD_checkSameManager(const BDD* this_ptr, const BDD* other);
 int BDD_Variable(BDD* this_ptr);
-BDD BDD_Then(const BDD* this_ptr);
-BDD BDD_Else(const BDD* this_ptr);
-BDD BDD_Exist(BDD* this_ptr, const BDD* cube);
-BDD BDD_Universal(BDD* this_ptr, const BDD* cube);
-BDD BDD_Restrict(const BDD* this_ptr, const BDD* other);
-BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other);
-BDD BDD_Permute(const BDD* this_ptr, const vector<int>* permu);
-BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube);
+void BDD_Then(BDD* ret_ptr, const BDD* this_ptr);
+void BDD_Else(BDD* ret_ptr, const BDD* this_ptr);
+void BDD_Exist(BDD* ret_ptr, BDD* this_ptr, const BDD* cube);
+void BDD_Universal(BDD* ret_ptr, BDD* this_ptr, const BDD* cube);
+void BDD_Restrict(BDD* ret_ptr, const BDD* this_ptr, const BDD* other);
+void BDD_Compose(BDD* ret_ptr, const BDD* this_ptr, int v, const BDD* other);
+void BDD_Permute(BDD* ret_ptr, const BDD* this_ptr, const vector<int>* permu);
+void BDD_AndExist(BDD* ret_ptr, BDD* this_ptr, const BDD* other, const BDD* cube);
 bool BDD_IsComp(BDD* this_ptr);
 const XManager* BDD_manager(const BDD* this_ptr);
 
 // In C we can not overload operators, so we use functions instead.
-BDD BDD_Operator_Not       (const BDD* this_ptr); // !
+void BDD_Operator_Not       (BDD* ret_ptr, const BDD* this_ptr); // !
+
 bool BDD_Operator_Equal    (const BDD* this_ptr, const BDD* other); // ==
-BDD BDD_Operator_Or        (const BDD* this_ptr, const BDD* other); // +
-BDD BDD_Operator_And       (const BDD* this_ptr, const BDD* other); // *
-BDD BDD_Operator_Xor       (const BDD* this_ptr, const BDD* other); // ^
-BDD BDD_Operator_LessEqual (const BDD* this_ptr, const BDD* other); // <=
-BDD BDD_Operator_Nor       (const BDD* this_ptr, const BDD* other); // %
-BDD BDD_Operator_Nand      (const BDD* this_ptr, const BDD* other); // |
-BDD BDD_Operator_XNor      (const BDD* this_ptr, const BDD* other); // &
+void BDD_Operator_Or        (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // +
+void BDD_Operator_And       (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // *
+void BDD_Operator_Xor       (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // ^
+void BDD_Operator_LessEqual (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // <=
+void BDD_Operator_Nor       (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // %
+void BDD_Operator_Nand      (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // |
+void BDD_Operator_XNor      (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // &
 
+
 XBDDManager* XBDDManager_new(int varCount);
-BDD XBDDManager_BddOne(XBDDManager* this_ptr);
-BDD XBDDManager_BddZero(XBDDManager* this_ptr);
-BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex);
-BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h);
+void XBDDManager_BddOne(BDD* ret_ptr, XBDDManager* this_ptr);
+void XBDDManager_BddZero(BDD* ret_ptr, XBDDManager* this_ptr);
+void XBDDManager_BddVar(BDD* ret_ptr, XBDDManager* this_ptr, int varIndex);
+void XBDDManager_Ite(BDD* ret_ptr, XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h);
 
-void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime);
+void XBDDManager_ShowInfo(XBDDManager* this_ptr);
 
 const XManager* XBDDManager_manager(const XBDDManager* this_ptr);
 }
diff --git a/hs/Data/HasCacBDD.hs b/hs/Data/HasCacBDD.hs
--- a/hs/Data/HasCacBDD.hs
+++ b/hs/Data/HasCacBDD.hs
@@ -20,6 +20,8 @@
   firstVarOf, maxVarOf, allVarsOf, allVarsOfSorted,
   -- * Sub-BDDs and length
   thenOf, elseOf, subsOf, sizeOf,
+  -- * Variable Orderings
+  optimalOrder,
   -- * Show and convert to trees
   BddTree(..), unravel, ravel,
   -- * Print some debugging information
@@ -31,7 +33,8 @@
 import Foreign.Ptr (Ptr)
 import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)
 import System.IO.Unsafe (unsafePerformIO)
-import Data.List (nub,(\\),sort)
+import Data.Function (on)
+import Data.List ((\\), minimumBy, nub, permutations, sort)
 import Data.Maybe (fromJust)
 import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf)
 
@@ -52,16 +55,16 @@
 type CacXBddManager = ()
 newtype XBddManager = XBddManager (ForeignPtr CacXBddManager)
 
-type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO (Ptr CacBDD)
-type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)
-type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)
+type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO ()
+type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO ()
+type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO ()
 
-foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: Word -> IO (Ptr CacBDD)
+foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: IO (Ptr CacBDD)
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_new" xBddManager_new :: CInt -> IO (Ptr CacXBddManager)
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_ShowInfo" xBddManager_showInfo :: Ptr CacXBddManager -> IO ()
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddOne"  xBddManager_BddOne  :: NullOp
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddZero" xBddManager_BddZero :: NullOp
-foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar"  xBddManager_BddVar  :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO (Ptr CacBDD)
+foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar"  xBddManager_BddVar  :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO ()
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_Ite"     xBddManager_Ite     :: Ptr CacBDD -> Ptr CacXBddManager -> BinaryOp
 foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Equal"  bdd_Operator_Equal  :: Ptr CacBDD -> Ptr CacBDD -> IO Bool
 foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Not"    bdd_Operator_Not    :: UnaryOp
@@ -85,19 +88,25 @@
 
 fromManager :: NullOp -> Bdd
 fromManager nulloperator = let (XBddManager mptr) = manager in
-  finalize $ unsafePerformIO $
-    withForeignPtr mptr $ nulloperator (unsafePerformIO (bdd_new 8))
+  finalize $ unsafePerformIO $ do
+    b <- bdd_new
+    withForeignPtr mptr $ nulloperator b
+    return b
 {-# NOINLINE fromManager #-}
 
 withBDD :: UnaryOp -> Bdd -> Bdd
-withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $
-  withForeignPtr fptr $ unioperator (unsafePerformIO (bdd_new 8))
+withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $ do
+  b <- bdd_new
+  withForeignPtr fptr $ unioperator b
+  return b
 {-# NOINLINE withBDD #-}
 
 withTwoBDDs :: BinaryOp -> Bdd -> Bdd -> Bdd
-withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $
+withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $ do
+  b <- bdd_new
   withForeignPtr fptr1 $
-    withForeignPtr fptr2 . binoperator (unsafePerformIO (bdd_new 8))
+    withForeignPtr fptr2 . binoperator b
+  return b
 {-# NOINLINE withTwoBDDs #-}
 
 fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a
@@ -165,11 +174,13 @@
 ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
 ifthenelse (Bdd test) (Bdd yes) (Bdd no) =
   let (XBddManager mptr) = manager in
-    finalize $ unsafePerformIO $
+    finalize $ unsafePerformIO $ do
+      b <- bdd_new
       withForeignPtr test (\t ->
         withForeignPtr yes (\y ->
           withForeignPtr no (\n ->
-            withForeignPtr mptr (\m -> xBddManager_Ite (unsafePerformIO (bdd_new 8)) m t y n))))
+            withForeignPtr mptr (\m -> xBddManager_Ite b m t y n))))
+      return b
 {-# NOINLINE ifthenelse #-}
 
 instance Eq Bdd where
@@ -268,7 +279,7 @@
       m1 = maxVarOf $ thenOf b
       m2 = maxVarOf $ elseOf b
 
--- | All variables in a given BDD, *not* sorted, lazy.
+-- | All variables in a given BDD, /not/ sorted, lazy.
 allVarsOf :: Bdd -> [Int]
 allVarsOf b
   | b == bot = []
@@ -282,7 +293,7 @@
 allVarsOfSorted = sort . allVarsOf
 
 -- | List all node / sub-BDDs of a given BDD.
--- This includes the root node of b itself, but omits terminal nodes.
+-- This includes the root node, but omits terminal nodes.
 subsOf :: Bdd -> [Bdd]
 subsOf = subsOf' [] where
   subsOf' done b
@@ -365,13 +376,13 @@
     addvars s = allvars \\ sort (map fst s)
     extend s v = [ (v,False):s, (v,True):s ]
 
--- | Get all complete assignments, given a set of all variables.
+-- | Get all complete assignments, given a list of variables.
 -- In particular this will include variables not in the BDD.
 allSatsWith :: [Int] -> Bdd -> [Assignment]
 allSatsWith allvars b = concatMap (completeAss allvars) (allSats b)
 
--- | Given a set of all variables, get the number of satisfying assignments.
--- Note that allvars must be nub'd and sorted.
+-- | Get the number of satisfying assignments, given a list of variables.
+-- Note that the given list must be nub'd and sorted.
 satCountWith :: [Int] -> Bdd -> Int
 satCountWith allvars b
   | b == top = 2 ^ length allvars
@@ -427,6 +438,12 @@
     Just k  -> case lookup k repls of
       Nothing  -> ifthenelse (var k) (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)
       Just psi -> ifthenelse psi     (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)
+
+-- | Find an optimal variable-reording.
+-- Returns a relabelling @r@ such that @sizeOf (relabel r b)@ is minimal.
+optimalOrder :: Bdd -> [(Int,Int)]
+optimalOrder b = minimumBy (compare `on` (\r -> sizeOf (relabel r b))) allPermut where
+  allPermut = map (zip (allVarsOf b)) $ permutations (allVarsOf b)
 
 -- | Show internal statistics.
 showInfo :: IO ()
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,3 +1,3 @@
-resolver: lts-21.19
+resolver: lts-21.25
 packages:
 - '.'
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -1,7 +1,7 @@
 module Main where
 
 import Data.HasCacBDD
-import Data.List (nub)
+import Data.List ((\\),nub)
 import Data.Maybe (fromJust,isNothing)
 import Data.Tuple (swap)
 import Test.QuickCheck
@@ -118,11 +118,17 @@
                                       relabel gnippam (relabel mapping b) == b)
     prop "relabelFun"    (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) == a)
     prop "substit"       (\b c -> substit 5 b c == ifthenelse b (restrict c (5,True)) (restrict c (5,False)))
+    prop "substit2"      (\b c -> substit (head ([0..] \\ allVarsOf c)) b c == c)
+    prop "substitSimul"  (\b -> substitSimul [] b == b)
+    prop "substitSimul2" (\b n -> substitSimul [(n,var n)] b == b)
+    prop "optimalOrder"  (\b -> sizeOf b < 15 ==> sizeOf (relabel (optimalOrder b) b) <= sizeOf b)
     prop "show"          (\a b -> (show a == show b) == (a == (b::Bdd)))
     prop "read"          (\b -> read (show b) == (b :: Bdd))
     prop "showList"      (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))
     prop "readList"      (\a b -> readList (show [a,b]) == [([unravel a, unravel b] :: [BddTree], "")])
   describe "QuickCheck Expected Failures" $ do
+    prop "evaluate may return Nothing" $
+      expectFailure (\b ass -> evaluate b ass =/= Nothing)
     prop "wrong deMorganOne" $
       expectFailure (\a b -> neg (a `con` b) === (neg a `con` neg b))
     prop "wrong deMorganTwo" $
