diff --git a/executable/Main.hs b/executable/Main.hs
--- a/executable/Main.hs
+++ b/executable/Main.hs
@@ -605,7 +605,11 @@
   hSetBuffering stdout LineBuffering
   join . parseCommandLineWithExtraArgs
     ["--no-conjunctive-conjectures", "--no-split"]
+#ifdef VERSION_twee
     "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $
+#else
+    "Twee, an equational theorem prover" . version "twee development version" $
+#endif
       globalFlags *> parseMainFlags *>
       -- hack: get --quiet and --no-proof options to appear before --tstp
       forAllFilesBox <*>
diff --git a/tests/ROB033-1.p b/tests/ROB033-1.p
new file mode 100644
--- /dev/null
+++ b/tests/ROB033-1.p
@@ -0,0 +1,10 @@
+cnf(commutativity_of_add, axiom, add(X, Y)=add(Y, X)).
+cnf(associativity_of_add, axiom,
+    add(add(X, Y), Z)=add(X, add(Y, Z))).
+cnf(robbins_axiom, axiom,
+    negate(add(negate(add(X, Y)), negate(add(X, negate(Y)))))=X).
+cnf(sos04, axiom, g(A)=negate(add(A, negate(A)))).
+cnf(sos05, axiom, h(A)=add(A, add(A, add(A, g(A))))).
+cnf(goals, negated_conjecture,
+    add(negate(add(x0, negate(x1))),
+        negate(add(negate(x0), negate(x1))))!=x1).
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.1.3
+version:             2.1.4
 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.3,
+                       twee-lib == 2.1.4,
                        containers,
                        pretty,
                        split,