diff --git a/.gitignore b/.gitignore
index 0d49d6b..4394b95 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,4 +3,6 @@ dist/
 *.o
 *.hi
 *.prof
+*.code-workspace
+bench.csv
 
diff --git a/bench/Bench.hs b/bench/Bench.hs
index 05e80b1..444b34d 100644
--- a/bench/Bench.hs
+++ b/bench/Bench.hs
@@ -1,23 +1,93 @@
-{-# OPTIONS_GHC -Wno-missing-signatures #-}
-import Bollig
+{-# language PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-partial-type-signatures #-}
+import Angluin (learnAngluin, learnAngluinRows)
+import Bollig (learnBollig)
 import Examples
 import Teacher
 
 import Gauge.Main
 import Gauge.Main.Options
+import NLambda
+
+{- Benchmarks can be run with `stack bench`. If you would like to run a
+   subset of benchmarks, you can do this with `stack bench --ba NomNLStar`
+   for example. May take a long time (so we only run once).
+
+   Note that we are using the whitebox equivalence checks, which may not
+   reflect "realistic" runtinme, because the representation of the
+   counterexamples is different.
+
+   The nondeterministic benchmarks are a bit subtle, because equivalence
+   is not decidable. We do a bounded bisimulation check, the bounds are
+   guessed to be sufficient, but not proven to be.
+
+   Examples.example4 is not used, because it takes a bit too long.
+-}
 
--- Run a single test since these are slow benchmarks
 myConfig = defaultConfig
   { quickMode = True
   , includeFirstIter = True
   , csvFile = Just "bench.csv"
   }
 
-main = defaultMainWith myConfig [
-  bgroup "NomNLStar"
-    [ bench "NFA1    " $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 2 Examples.exampleNFA1)
-    , bench "NFA2 1  " $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 3 (Examples.exampleNFA2 1))
-    , bench "NFA2 2  " $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 4 (Examples.exampleNFA2 2))
-    , bench "Residual" $ whnf (learnBollig 1 0) (teacherWithTargetNonDet 2 Examples.exampleResidual1)
+-- Some bounds on the size of automata
+fifoBound = 4
+stackBound = 4
+doublewordBound = 3
+nlastpositionBound = 4
+
+main = defaultMainWith myConfig
+  [ bgroup "NomLStarR"
+    [ bgroup "Fifo" $
+      fmap (\n -> bench (show n) $ whnf lstar (target (fifoExample n))) [0..fifoBound]
+    , bgroup "Stack" $
+      fmap (\n -> bench (show n) $ whnf lstar (target (stackExample n))) [0..stackBound]
+    , bgroup "Double Word" $
+      fmap (\n -> bench (show n) $ whnf lstar (target (runningExample atoms n))) [0..doublewordBound]
+    , bgroup "n-last Position" $
+      fmap (\n -> bench (show n) $ whnf lstar (targetNonDet (n+2) (exampleNFA2 n))) [0..nlastpositionBound]
+    , bench "example1" $ whnf lstar (target example1)
+    , bench "example2" $ whnf lstar (target example2)
+    , bench "example3" $ whnf lstar (target example3)
+    --, bench "example4" $ whnf lstar (target example4)
+    , bench "example5" $ whnf lstar (target example5)
+    ]
+  , bgroup "NomLStarC"
+    [ bgroup "Fifo" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (target (fifoExample n))) [0..fifoBound]
+    , bgroup "Stack" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (target (stackExample n))) [0..stackBound]
+    , bgroup "Double Word" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (target (runningExample atoms n))) [0..doublewordBound]
+    , bgroup "n-last Position" $
+      fmap (\n -> bench (show n) $ whnf lstarCol (targetNonDet (n+2) (exampleNFA2 n))) [0..nlastpositionBound]
+    , bench "example1" $ whnf lstarCol (target example1)
+    , bench "example2" $ whnf lstarCol (target example2)
+    , bench "example3" $ whnf lstarCol (target example3)
+    --, bench "example4" $ whnf lstarCol (target example4)
+    , bench "example5" $ whnf lstarCol (target example5)
+    ]
+  , bgroup "NomNLStar"
+    [ bgroup "n-last Position" $
+      fmap (\n -> bench (show n) $ whnf nlstar (targetNonDet (n+2) (exampleNFA2 n))) [0..nlastpositionBound]
+    , bench "example1" $ whnf nlstar (targetNonDet 3 example1)
+    , bench "example2" $ whnf nlstar (targetNonDet 2 example2)
+    , bench "example3" $ whnf nlstar (targetNonDet 2 example3)
+    --, bench "example4" $ whnf nlstar (targetNonDet 4 example4)
+    , bench "example5" $ whnf nlstar (targetNonDet 3 example5)
+    , bench "NFA1    " $ whnf nlstar (targetNonDet 2 exampleNFA1)
+    , bench "Residual" $ whnf nlstar (targetNonDet 2 exampleResidual1)
     ]
   ]
+
+-- Some (polymorphic) abbreviations
+lstar, lstarCol, nlstar :: _ => Teacher i -> Automaton _ i
+lstar = learnAngluinRows
+lstarCol = learnAngluin
+nlstar = learnBollig 0 0
+
+target :: _ => Automaton q i -> Teacher i
+target = teacherWithTarget
+
+targetNonDet :: _ => Int -> Automaton q i -> Teacher i
+targetNonDet = teacherWithTargetNonDet
diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal
index ef99a39..653d9aa 100644
--- a/nominal-lstar.cabal
+++ b/nominal-lstar.cabal
@@ -60,3 +60,12 @@ benchmark bench
   build-depends:
     gauge,
     nominal-lstar
+
+test-suite test
+  import: stuff
+  hs-source-dirs: test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  build-depends:
+    gauge,
+    nominal-lstar
diff --git a/src/Angluin.hs b/src/Angluin.hs
index aec61ad..3231448 100644
--- a/src/Angluin.hs
+++ b/src/Angluin.hs
@@ -10,8 +10,10 @@ import Debug.Trace
 import NLambda
 import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.))
 
+-- This was actually a pessimisation (often), also it sometimes crashes.
+-- So I changed it to a no-op.
 justOne :: (Contextual a, NominalType a) => Set a -> Set a
-justOne = mapFilter id . orbit [] . element
+justOne = id -- mapFilter id . orbit [] . element
 
 -- We can determine its completeness with the following
 -- It returns all witnesses (of the form sa) for incompleteness
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
index 0000000..46ae0e4
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,27 @@
+{-# language PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-partial-type-signatures #-}
+import Angluin (learnAngluin)
+import Examples
+import Teacher
+
+import Gauge.Main
+import Gauge.Main.Options
+import NLambda
+
+{- TODO: choose test framework -}
+
+myConfig = defaultConfig
+  { quickMode = True
+  , includeFirstIter = True
+  , csvFile = Just "test.csv"
+  }
+
+main = defaultMainWith myConfig
+  [ bench "DW2" $ whnf lstarCol (target (runningExample atoms 2)) ]
+
+-- Some (polymorphic) abbreviations
+lstarCol :: _ => Teacher i -> Automaton _ i
+lstarCol = learnAngluin
+
+target :: _ => Automaton q i -> Teacher i
+target = teacherWithTarget