diff --git a/tests/cm.p b/tests/cm.p
new file mode 100644
--- /dev/null
+++ b/tests/cm.p
@@ -0,0 +1,3 @@
+fof(a, axiom, ![X, Y]: plus(X, Y)=plus(Y, X)).
+fof(a, axiom, ![X, Y, Z]: plus(plus(X, Y), Z)=plus(X, plus(Z, Y))).
+fof(a, axiom, a!=b).
diff --git a/tests/y-easy.p b/tests/y-easy.p
new file mode 100644
--- /dev/null
+++ b/tests/y-easy.p
@@ -0,0 +1,4 @@
+fof(k_def, axiom, ![X, Y]: (k @ X) @ Y = X).
+fof(s_def, axiom, ![X, Y, Z]: ((s @ X) @ Y) @ Z = (X @ Z) @ (Y @ Z)).
+fof(i_def, axiom, ![X]: i @ X = X).
+fof(conjecture, conjecture, ?[Y]: ![F]: Y @ F = F @ (Y @ F)).
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.4.1
+version:             2.4.2
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -45,7 +45,7 @@
   other-modules:       SequentialMain
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.4.1,
+                       twee-lib == 2.4.2,
                        containers,
                        pretty,
                        split,