diff --git a/library/tools/super/clausifier.lean b/library/tools/super/clausifier.lean
index fc755ce154..9a184f44b1 100644
--- a/library/tools/super/clausifier.lean
+++ b/library/tools/super/clausifier.lean
@@ -269,7 +269,14 @@ local_false ← target,
 l ← local_context,
 monad.for l (clause.of_proof local_false)
 
-@[super.inf]
+meta def clausify_pre := preprocessing_rule $ take new, lift list.join $ for new $ λ dc, do
+cs ← get_clauses_classical [dc^.c],
+if cs^.length ≤ 1 then
+  return (for cs $ λ c, { dc with c := c })
+else
+  for cs (λc, mk_derived c dc^.sc)
+
+-- @[super.inf]
 meta def clausification_inf : inf_decl := inf_decl.mk 0 $
 λgiven, list.foldr orelse (return ()) $
         do r ← clausification_rules_classical,
diff --git a/library/tools/super/prover.lean b/library/tools/super/prover.lean
index ba3110b4ed..03a64b69a8 100644
--- a/library/tools/super/prover.lean
+++ b/library/tools/super/prover.lean
@@ -74,6 +74,7 @@ run_prover_loop (i+1)
 
 meta def default_preprocessing : list (prover unit) :=
 [
+clausify_pre,
 factor_dup_lits_pre,
 remove_duplicates_pre,
 refl_r_pre,