diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.14
+Version: 0.5.15
 Cabal-version: >= 1.10
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/Tools/Clausify.hs b/src/Jukebox/Tools/Clausify.hs
--- a/src/Jukebox/Tools/Clausify.hs
+++ b/src/Jukebox/Tools/Clausify.hs
@@ -118,8 +118,8 @@
 -- core clausification algorithm
 
 clausForm :: AxKind -> Input Form -> M [Input Clause]
-clausForm _ inp
-  | Just clause <- toClause (what inp) =
+clausForm k inp
+  | Just clause <- toClause (what inp), kind inp == Ax k =
     return [fmap (const clause) inp]
 clausForm kind inp =
   withName (tag inp) $