diff --git a/tests/fol.p b/tests/fol.p
new file mode 100644
--- /dev/null
+++ b/tests/fol.p
@@ -0,0 +1,16 @@
+cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B).
+cnf(ifeq_axiom, axiom, ifeq(X2, X2, U2, V2)=U2).
+cnf(ifeq_axiom, axiom, ifeq(X2, Y2, U2, U2)=U2).
+cnf(ifeq_axiom, axiom, ifeq(X2, Y2, X2, Y2)=Y2).
+cnf(ifeq_axiom, axiom,
+    ifeq(ifeq(U2, V2, A4, B4), ifeq(U2, V2, A3, B3),
+          ifeq(U2, V2, A, B), ifeq(U2, V2, A2, B2))=ifeq(U2, V2,
+                                                            ifeq(A4, A3, A, A2),
+                                                            ifeq(B4, B3, B, B2))).
+cnf(ifeq_axiom, axiom,
+    ifeq(X2, Y2, ifeq(X2, Y2, U2, V2),
+          ifeq(X2, Y2, S2, T2))=ifeq(X2, Y2, U2, T2)).
+cnf(a, axiom, ifeq(p, true, q, true)=q).
+cnf(a, negated_conjecture, ifeq(q, true, a, b)=b).
+cnf(a_1, negated_conjecture, ifeq(p, true, a, b)=b).
+cnf(goal, negated_conjecture, a!=b).
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.1.1
+version:             2.1.2
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -44,7 +44,7 @@
   main-is:             executable/Main.hs
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.1.1,
+                       twee-lib == 2.1.2,
                        containers,
                        pretty,
                        split,