feat(tools/super): clausify during preprocessing

Some inference produce terms with large useless redexes such as
(prod.fst (prod.mk _ _)).  Since we do normalization during
preprocessing, we can avoid ever even looking at these terms.

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,

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,