diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel
index c1c447036c..0820d99794 100644
--- a/ortools/sat/BUILD.bazel
+++ b/ortools/sat/BUILD.bazel
@@ -1638,6 +1638,7 @@ cc_library(
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
         "//ortools/util:time_limit",
+        "@abseil-cpp//absl/algorithm:container",
         "@abseil-cpp//absl/cleanup",
         "@abseil-cpp//absl/container:btree",
         "@abseil-cpp//absl/container:flat_hash_map",
diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc
index f0ef8f42ce..7b1b47078e 100644
--- a/ortools/sat/clause.cc
+++ b/ortools/sat/clause.cc
@@ -125,7 +125,6 @@ ClauseManager::~ClauseManager() {
 }
 
 void ClauseManager::Resize(int num_variables) {
-  DCHECK(is_clean_);
   watchers_on_false_.resize(num_variables << 1);
   reasons_.resize(num_variables);
   needs_cleaning_.Resize(LiteralIndex(num_variables << 1));
@@ -980,8 +979,29 @@ bool BinaryImplicationGraph::AddBinaryClauseInternal(
     trail_->ChangeReason(trail_index, propagator_id_);
   }
 
+  // Deal with literal fixing and do not even add a binary clause in that case.
   if (rep_a == rep_b) {
     return FixLiteral(rep_a, {rep_id});
+  } else if (trail_->CurrentDecisionLevel() == 0) {
+    const auto& assignment = trail_->Assignment();
+
+    // TODO(user): just make GetUnitClauseId() work all the time? for that
+    // we need to make sure all level zero are pushed with kUnitReason.
+    if (lrat_proof_handler_ != nullptr) {
+      if (assignment.LiteralIsFalse(rep_a)) {
+        return FixLiteral(rep_b,
+                          {rep_id, trail_->GetUnitClauseId(rep_a.Variable())});
+      } else if (assignment.LiteralIsFalse(rep_b)) {
+        return FixLiteral(rep_a,
+                          {rep_id, trail_->GetUnitClauseId(rep_b.Variable())});
+      }
+    } else {
+      if (assignment.LiteralIsFalse(rep_a)) {
+        return FixLiteral(rep_b, {});
+      } else if (assignment.LiteralIsFalse(rep_b)) {
+        return FixLiteral(rep_a, {});
+      }
+    }
   }
 
   a = rep_a;
diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
index 0de2876757..74be2c2ba6 100644
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -284,15 +284,6 @@ std::string ValidateLinearExpression(const CpModelProto& model,
   return "";
 }
 
-std::string ValidateConstantExpression(const CpModelProto& model,
-                                       const LinearExpressionProto& expr) {
-  if (!expr.vars().empty()) {
-    return absl::StrCat("expression must be constant: ",
-                        ProtobufShortDebugString(expr));
-  }
-  return ValidateLinearExpression(model, expr);
-}
-
 std::string ValidateLinearConstraint(const CpModelProto& model,
                                      const ConstraintProto& ct) {
   if (!DomainInProtoIsValid(ct.linear())) {
@@ -1376,8 +1367,8 @@ class ConstraintChecker {
   bool LinearConstraintIsFeasible(const ConstraintProto& ct) {
     int64_t sum = 0;
     const int num_variables = ct.linear().coeffs_size();
-    const int* const vars = ct.linear().vars().data();
-    const int64_t* const coeffs = ct.linear().coeffs().data();
+    absl::Span<const int> vars = absl::MakeSpan(ct.linear().vars());
+    absl::Span<const int64_t> coeffs = absl::MakeSpan(ct.linear().coeffs());
     for (int i = 0; i < num_variables; ++i) {
       // We know we only have positive reference now.
       DCHECK(RefIsPositive(vars[i]));
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index a116cb39b6..0ab1659014 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -2529,6 +2529,12 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   }
 #endif  // ORTOOLS_TARGET_OS_SUPPORTS_THREADS
 
+  if (DEBUG_MODE) {
+    LOG(WARNING)
+        << "WARNING: CP-SAT is running in debug mode. The solver will "
+           "be slow because we will do a lot of extra checks. Compile in "
+           "optimization mode to gain an order of magnitude speedup.";
+  }
   SOLVER_LOG(logger, "");
   SOLVER_LOG(logger, "Starting ", CpSatSolverVersion());
   SOLVER_LOG(logger, "Parameters: ", ProtobufShortDebugString(params));
diff --git a/ortools/sat/csharp/CpSolver.cs b/ortools/sat/csharp/CpSolver.cs
index 9a5a89dc42..1e8fc491c5 100644
--- a/ortools/sat/csharp/CpSolver.cs
+++ b/ortools/sat/csharp/CpSolver.cs
@@ -210,7 +210,8 @@ public class CpSolver : IDisposable
     /// <summary>
     /// Releases unmanaged resources and optionally releases managed resources.
     /// </summary>
-    /// <param name="disposing">true to release both managed and unmanaged resources; false to release only unmanaged resources.</param>
+    /// <param name="disposing">true to release both managed and unmanaged resources; false to release only unmanaged
+    /// resources.</param>
     protected virtual void Dispose(bool disposing)
     {
         if (_disposed)
@@ -270,4 +271,4 @@ class BestBoundCallbackDelegate : BestBoundCallback
     public override void NewBestBound(double bound) => _delegate(bound);
 }
 
-} // namespace Google.OrTools.Sat
\ No newline at end of file
+} // namespace Google.OrTools.Sat
diff --git a/ortools/sat/gate_utils.h b/ortools/sat/gate_utils.h
index d902c57977..0674556f17 100644
--- a/ortools/sat/gate_utils.h
+++ b/ortools/sat/gate_utils.h
@@ -98,6 +98,28 @@ inline int AddHoleAtPosition(int i, int bitset) {
   return (bitset & ((1 << i) - 1)) + ((bitset >> i) << (i + 1));
 }
 
+inline int RemoveFixedInput(int i, bool at_true,
+                            absl::Span<LiteralIndex> inputs,
+                            int& int_function_values) {
+  DCHECK_LT(i, inputs.size());
+  const int value = at_true ? 1 : 0;
+
+  // Re-compute the bitset.
+  SmallBitset values = int_function_values;
+  SmallBitset new_truth_table = 0;
+  const int new_size = inputs.size() - 1;
+  for (int p = 0; p < (1 << new_size); ++p) {
+    const int extended_p = AddHoleAtPosition(i, p) | (value << i);
+    new_truth_table |= ((values >> extended_p) & 1) << p;
+  }
+  int_function_values = new_truth_table;
+
+  for (int j = i + 1; j < inputs.size(); ++j) {
+    inputs[j - 1] = inputs[j];
+  }
+  return new_size;
+}
+
 // The function is target = function_values[inputs as bit position].
 //
 // TODO(user): This can be optimized with more bit twiddling if needed.
diff --git a/ortools/sat/gate_utils_test.cc b/ortools/sat/gate_utils_test.cc
index 1294122b2b..07428e2190 100644
--- a/ortools/sat/gate_utils_test.cc
+++ b/ortools/sat/gate_utils_test.cc
@@ -75,6 +75,47 @@ TEST(AddHoleAtPositionTest, BasicTest) {
   EXPECT_EQ(AddHoleAtPosition(8, 0xFF), 0b011111111);
 }
 
+TEST(CanonicalizeFunctionTruthTableTest, AndGateWithXAndNotX) {
+  LiteralIndex output = Literal(+1).Index();
+  std::vector<LiteralIndex> inputs{Literal(+2).Index(), Literal(-2).Index()};
+  int table = 0b1000;
+  const int new_size =
+      CanonicalizeFunctionTruthTable(output, absl::MakeSpan(inputs), table);
+  CHECK_EQ(new_size, 0);  // Fixed to zero.
+}
+
+TEST(RemoveFixedInputTest, BasicTest1) {
+  std::vector<LiteralIndex> inputs{Literal(+1).Index(), Literal(+2).Index(),
+                                   Literal(+3).Index()};
+  int table = 0b01011010;
+  const int new_size = RemoveFixedInput(1, true, absl::MakeSpan(inputs), table);
+  EXPECT_EQ(new_size, 2);
+  EXPECT_EQ(inputs[0], Literal(+1).Index());
+  EXPECT_EQ(inputs[1], Literal(+3).Index());
+  EXPECT_EQ(table, 0b0110) << std::bitset<4>(table);
+}
+
+TEST(RemoveFixedInputTest, BasicTest2) {
+  std::vector<LiteralIndex> inputs{Literal(+1).Index(), Literal(+2).Index(),
+                                   Literal(+3).Index()};
+  int table = 0b01011010;
+  const int new_size =
+      RemoveFixedInput(1, false, absl::MakeSpan(inputs), table);
+  EXPECT_EQ(new_size, 2);
+  EXPECT_EQ(inputs[0], Literal(+1).Index());
+  EXPECT_EQ(inputs[1], Literal(+3).Index());
+  EXPECT_EQ(table, 0b0110) << std::bitset<4>(table);
+}
+
+TEST(CanonicalizeFunctionTruthTableTest, AndGateWithXAndNotX2) {
+  LiteralIndex output = Literal(+1).Index();
+  std::vector<LiteralIndex> inputs{Literal(-2).Index(), Literal(+2).Index()};
+  int table = 0b1000;
+  const int new_size =
+      CanonicalizeFunctionTruthTable(output, absl::MakeSpan(inputs), table);
+  CHECK_EQ(new_size, 0);  // Fixed to zero.
+}
+
 TEST(CanonicalizeFunctionTruthTableTest, RandomTest) {
   absl::BitGen random;
   const int num_vars = 8;
diff --git a/ortools/sat/lrat_proof_handler.cc b/ortools/sat/lrat_proof_handler.cc
index f722c9d992..d2a226b103 100644
--- a/ortools/sat/lrat_proof_handler.cc
+++ b/ortools/sat/lrat_proof_handler.cc
@@ -802,7 +802,6 @@ ClauseId LratProofHandler::AddAndProveInferredClauseByEnumeration(
   // That give us 2^(n + 1) intermediate clauses.
   // Their ids will be stored in (1 << k) + binary_encoding_of_the_li.
   const int n = to_dense_index.size() - new_clause.size();
-  CHECK_GT(n, 0);  // We dealt with this above.
   CHECK_EQ(n, relevant_literals.size());
   const int num_intermediates = 1 << (n + 1);
   std::vector<ClauseId> ids(num_intermediates, kNoClauseId);
@@ -838,11 +837,16 @@ ClauseId LratProofHandler::AddAndProveInferredClauseByEnumeration(
       // The clause is the same as the one we try to prove! or smaller.
       if (clauses_for_proof[i].size() == new_clause.size()) {
         return ids_for_proof[i];
+      } else {
+        // TODO(user): Likely we could have simplified what we are trying to
+        // prove. Like I saw this happen when we prove an equivalence but we
+        // can actually prove that the variables are fixed.
+        const ClauseId new_id = id_generator_->GetNextId();
+        if (!AddInferredClause(new_id, new_clause, {ids_for_proof[i]})) {
+          return error("failed trivial inclusion proof");
+        }
+        return new_id;
       }
-
-      // TODO(user): if this ever happen we can create a new id and prove it
-      // with clauses_for_proof[i], but for now I never saw that.
-      return error("Case not yet supported");
     }
 
     mask >>= new_clause.size();
diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc
index 79ffa761e8..a7c8431584 100644
--- a/ortools/sat/probing.cc
+++ b/ortools/sat/probing.cc
@@ -14,11 +14,14 @@
 #include "ortools/sat/probing.h"
 
 #include <algorithm>
+#include <deque>
 #include <functional>
 #include <optional>
 #include <utility>
+#include <variant>
 #include <vector>
 
+#include "absl/algorithm/container.h"
 #include "absl/cleanup/cleanup.h"
 #include "absl/container/btree_map.h"
 #include "absl/container/btree_set.h"
@@ -51,6 +54,212 @@
 namespace operations_research {
 namespace sat {
 
+// Holds a copy of the trail and of propagator reasons in order to be able to
+// build LRAT proofs after the trail has been modified.
+class TrailCopy {
+ public:
+  TrailCopy(const Trail& trail, const BinaryImplicationGraph& implication_graph,
+            const ClauseManager& clause_manager)
+      : trail_(trail),
+        implication_graph_(implication_graph),
+        clause_manager_(clause_manager) {}
+
+  // Updates this trail copy with the current trail state.
+  void CopyTrail() {
+    const int trail_size = trail_.Index();
+    trail_index_.resize(trail_.NumVariables(), -1);
+    trail_literals_.clear();
+    trail_info_.clear();
+    stored_reasons_.clear();
+    trail_literals_.reserve(trail_size);
+    trail_info_.reserve(trail_size);
+    for (int i = 0; i < trail_size; ++i) {
+      const Literal literal = trail_[i];
+      const BooleanVariable var = literal.Variable();
+      const AssignmentInfo& info = trail_.Info(var);
+      const int assignment_type = trail_.AssignmentType(var);
+      absl::Span<const Literal> reason;
+      // Get the clause ID only if it is very cheap to compute. Otherwise, delay
+      // its computation until it is really needed, in AppendClauseIdsFixing().
+      std::variant<ClauseId, const SatClause*> reason_clause = kNoClauseId;
+      if (assignment_type == AssignmentType::kCachedReason) {
+        const absl::Span<const Literal> cached_reason = trail_.Reason(var);
+        stored_reasons_.push_back({cached_reason.begin(), cached_reason.end()});
+        reason = stored_reasons_.back();
+      } else if (assignment_type == AssignmentType::kUnitReason) {
+        reason_clause = trail_.GetUnitClauseId(var);
+      } else if (assignment_type == implication_graph_.PropagatorId()) {
+        absl::Span<const Literal> original_reason = trail_.Reason(var);
+        DCHECK_EQ(original_reason.size(), 1);
+        reason = absl::MakeConstSpan(trail_literals_)
+                     .subspan(trail_index_[original_reason[0].Variable()], 1);
+        DCHECK_EQ(reason[0], original_reason[0].Negated());
+      } else if (assignment_type == clause_manager_.PropagatorId()) {
+        const SatClause* sat_clause = clause_manager_.ReasonClauseOrNull(var);
+        if (sat_clause != nullptr) {
+          reason = sat_clause->AsSpan();
+        }
+        reason_clause = clause_manager_.ReasonClauseOrNull(var);
+      }
+      trail_index_[var] = i;
+      trail_literals_.push_back(literal);
+      trail_info_.emplace_back(info.level, assignment_type, reason,
+                               reason_clause);
+    }
+
+    const int num_decisions = trail_.CurrentDecisionLevel();
+    decisions_.clear();
+    decisions_.reserve(num_decisions);
+    for (int i = 0; i < num_decisions; ++i) {
+      decisions_.push_back(trail_.Decisions()[i].literal);
+    }
+  }
+
+  // Same as ClauseManager::AppendClauseIdsFixing(), but adapted to work on this
+  // trail copy instead of on the real trail.
+  void AppendClauseIdsFixing(
+      absl::Span<const Literal> literals, std::vector<ClauseId>* clause_ids,
+      LiteralIndex decision,
+      absl::flat_hash_map<std::pair<Literal, Literal>, ClauseId>
+          tmp_binary_clause_ids) {
+    // Mark the literals whose reason must be expanded, and put them in a heap.
+    tmp_mark_.ClearAndResize(BooleanVariable(trail_index_.size()));
+    marked_trail_indices_heap_.clear();
+    for (const Literal lit : literals) {
+      tmp_mark_.Set(lit.Variable());
+      marked_trail_indices_heap_.push_back(trail_index_[lit.Variable()]);
+    }
+    absl::c_make_heap(marked_trail_indices_heap_);
+    const int current_level = decisions_.size();
+
+    // The min level of the expanded literals.
+    int min_level = current_level;
+
+    // Unit clauses must come first. We put them in clause_ids directly. We put
+    // the others in non_unit_clause_ids and append them to clause_ids at the
+    // end.
+    std::vector<ClauseId>& non_unit_clause_ids =
+        tmp_clause_ids_for_append_clauses_fixing_;
+    non_unit_clause_ids.clear();
+
+    while (!marked_trail_indices_heap_.empty()) {
+      absl::c_pop_heap(marked_trail_indices_heap_);
+      const int trail_index = marked_trail_indices_heap_.back();
+      marked_trail_indices_heap_.pop_back();
+      const Literal marked_literal = trail_literals_[trail_index];
+      const TrailInfo& trail_info = trail_info_[trail_index];
+
+      // Stop at decisions, at literals fixed at root, and at literals implied
+      // by the decision at their level.
+      const int level = trail_info.level;
+      if (level > 0) min_level = std::min(min_level, level);
+      if (trail_info.assignment_type == AssignmentType::kSearchDecision) {
+        continue;
+      }
+      if (level == 0) {
+        clause_ids->push_back(std::get<ClauseId>(trail_info.reason_clause));
+        continue;
+      }
+      const Literal level_decision = decisions_[level - 1];
+      ClauseId clause_id = implication_graph_.GetClauseId(
+          level_decision.Negated(), marked_literal);
+      if (clause_id == kNoClauseId) {
+        const auto it = tmp_binary_clause_ids.find(
+            std::minmax(level_decision.Negated(), marked_literal));
+        if (it != tmp_binary_clause_ids.end()) {
+          clause_id = it->second;
+        }
+      }
+      if (clause_id != kNoClauseId) {
+        non_unit_clause_ids.push_back(clause_id);
+        continue;
+      }
+
+      // Mark all the literals of its reason.
+      for (const Literal literal : trail_info.reason) {
+        const BooleanVariable var = literal.Variable();
+        if (!tmp_mark_[var]) {
+          const int trail_index = trail_index_[var];
+          const TrailInfo& info = trail_info_[trail_index];
+          tmp_mark_.Set(var);
+          if (info.level > 0) {
+            marked_trail_indices_heap_.push_back(trail_index);
+            absl::c_push_heap(marked_trail_indices_heap_);
+          } else {
+            clause_ids->push_back(std::get<ClauseId>(info.reason_clause));
+          }
+        }
+      }
+      non_unit_clause_ids.push_back(ReasonClauseId(trail_index));
+    }
+
+    // Add the implication chain from `decision` to all the decisions found
+    // during the expansion.
+    if (Literal(decision) != decisions_[current_level - 1]) {
+      // If `decision` is not the last decision, it must directly imply it.
+      clause_ids->push_back(implication_graph_.GetClauseId(
+          Literal(decision).Negated(), decisions_[current_level - 1]));
+    }
+    for (int level = current_level - 1; level >= min_level; --level) {
+      clause_ids->push_back(implication_graph_.GetClauseId(
+          decisions_[level].Negated(), decisions_[level - 1]));
+    }
+
+    clause_ids->insert(clause_ids->end(), non_unit_clause_ids.rbegin(),
+                       non_unit_clause_ids.rend());
+  }
+
+ private:
+  // Same as ClauseManager::ReasonClauseId(), but adapted to work on this trail
+  // copy instead of on the real trail.
+  ClauseId ReasonClauseId(int trail_index) const {
+    const TrailInfo& trail_info = trail_info_[trail_index];
+    const int assignment_type = trail_info.assignment_type;
+    if (assignment_type == AssignmentType::kCachedReason ||
+        assignment_type == AssignmentType::kUnitReason) {
+      return std::get<ClauseId>(trail_info.reason_clause);
+    } else if (assignment_type == implication_graph_.PropagatorId()) {
+      return implication_graph_.GetClauseId(trail_literals_[trail_index],
+                                            trail_info.reason[0].Negated());
+    } else if (assignment_type == clause_manager_.PropagatorId()) {
+      const SatClause* reason =
+          std::get<const SatClause*>(trail_info.reason_clause);
+      if (reason != nullptr) {
+        return clause_manager_.GetClauseId(reason);
+      }
+    }
+    return kNoClauseId;
+  }
+
+  struct TrailInfo {
+    int level;
+    int assignment_type;
+    // For literals propagated by the BinaryImplicationGraph, the negation of
+    // the original reason. For literals propagated by the ClauseManager, *all*
+    // the literals of the SatClause (which includes the propagated variable).
+    // For kCachedReason, this is the stored reason. Empty for kUnitReason.
+    absl::Span<const Literal> reason;
+    // Holds a clause ID if `assignment_type` is kCachedReason or kUnitReason,
+    // or a SatClause* if `assignment_type` corresponds to the ClauseManager.
+    std::variant<ClauseId, const SatClause*> reason_clause;
+  };
+
+  const Trail& trail_;
+  const BinaryImplicationGraph& implication_graph_;
+  const ClauseManager& clause_manager_;
+
+  util_intops::StrongVector<BooleanVariable, int> trail_index_;
+  std::vector<Literal> trail_literals_;
+  std::vector<TrailInfo> trail_info_;
+  // We use a deque for pointer stability (they are kept in TrailInfo::reason).
+  std::deque<std::vector<Literal>> stored_reasons_;
+  std::vector<Literal> decisions_;
+
+  SparseBitset<BooleanVariable> tmp_mark_;
+  std::vector<int> marked_trail_indices_heap_;
+  std::vector<ClauseId> tmp_clause_ids_for_append_clauses_fixing_;
+};
+
 Prober::Prober(Model* model)
     : trail_(*model->GetOrCreate<Trail>()),
       assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
@@ -63,11 +272,14 @@ Prober::Prober(Model* model)
       clause_manager_(model->GetOrCreate<ClauseManager>()),
       clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
       lrat_proof_handler_(model->Mutable<LratProofHandler>()),
+      trail_copy_(new TrailCopy(trail_, *implication_graph_, *clause_manager_)),
       drat_enabled_(lrat_proof_handler_ != nullptr &&
                     (lrat_proof_handler_->drat_check_enabled() ||
                      lrat_proof_handler_->drat_output_enabled())),
       logger_(model->GetOrCreate<SolverLogger>()) {}
 
+Prober::~Prober() { delete trail_copy_; }
+
 bool Prober::ProbeBooleanVariables(const double deterministic_time_limit) {
   const int num_variables = sat_solver_->NumVariables();
   const VariablesAssignment& assignment = sat_solver_->Assignment();
@@ -87,6 +299,12 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
   new_integer_bounds_.clear();
   propagated_.ResetAllToFalse();
   tmp_binary_clause_ids_.clear();
+  // We block clause deletion since we compute some LRAT proofs in a delayed
+  // way, and we need to make sure the clauses that were used are still around.
+  sat_solver_->BlockClauseDeletion(true);
+  absl::Cleanup unblock_clause_deletion = [&] {
+    sat_solver_->BlockClauseDeletion(false);
+  };
   for (const Literal decision : {Literal(b, true), Literal(b, false)}) {
     if (assignment_.LiteralIsAssigned(decision)) continue;
 
@@ -143,7 +361,7 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
     }
 
     if (lrat_proof_handler_ != nullptr) {
-      auto add_tmp_implication = [&](const Literal decision, const Literal l) {
+      for (const Literal l : new_implied_or_fixed_literals_) {
         tmp_clause_ids_.clear();
         clause_manager_->AppendClauseIdsFixing(
             {l}, &tmp_clause_ids_, decision.Index(),
@@ -161,23 +379,21 @@ bool Prober::ProbeOneVariableInternal(BooleanVariable b) {
         tmp_binary_clause_ids_[std::minmax(decision.Negated(), l)] = clause_id;
         num_lrat_clauses_++;
         num_lrat_proof_clauses_ += tmp_clause_ids_.size();
-      };
-      for (const Literal l : new_implied_or_fixed_literals_) {
-        add_tmp_implication(decision, l);
       }
-      if (decision.IsNegative() && !to_fix_at_true_.empty()) {
-        // Redo the first pass to add the LRAT clauses b => to_fix_at_true.
-        if (!sat_solver_->ResetToLevelZero()) return false;
-        if (assignment_.LiteralIsAssigned(decision)) continue;
-        CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
-        if (sat_solver_->EnqueueDecisionAndBackjumpOnConflict(
-                decision.Negated()) == kUnsatTrailIndex) {
-          return false;
-        }
-        if (sat_solver_->ModelIsUnsat()) return false;
-        if (sat_solver_->CurrentDecisionLevel() == 0) continue;
+      if (decision.IsPositive()) {
+        trail_copy_->CopyTrail();
+      } else if (!to_fix_at_true_.empty()) {
         for (const Literal l : to_fix_at_true_) {
-          add_tmp_implication(decision.Negated(), l);
+          tmp_clause_ids_.clear();
+          trail_copy_->AppendClauseIdsFixing({l}, &tmp_clause_ids_,
+                                             decision.NegatedIndex(),
+                                             tmp_binary_clause_ids_);
+          const ClauseId clause_id = clause_id_generator_->GetNextId();
+          lrat_proof_handler_->AddInferredClause(clause_id, {decision, l},
+                                                 tmp_clause_ids_);
+          tmp_binary_clause_ids_[std::minmax(decision, l)] = clause_id;
+          num_lrat_clauses_++;
+          num_lrat_proof_clauses_ += tmp_clause_ids_.size();
         }
       }
     }
@@ -980,6 +1196,8 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
   num_conflicts_ = 0;
   num_new_binary_ = 0;
   num_subsumed_ = 0;
+  num_lrat_clauses_ = 0;
+  num_lrat_proof_clauses_ = 0;
 
   // Reset the solver in case it was already used.
   if (!sat_solver_->ResetToLevelZero()) return false;
@@ -1030,12 +1248,14 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
   }
 
   binary_clause_extracted_.assign(trail_.Index(), false);
+  trail_implication_clauses_.assign(trail_.Index(), {kNoClauseId, false});
 
   while (!time_limit_->LimitReached() &&
          time_limit_->GetElapsedDeterministicTime() <= limit) {
     // We only enqueue literal at level zero if we don't use "tree look".
     if (!options.use_tree_look) {
       if (!sat_solver_->BacktrackAndPropagateReimplications(0)) return false;
+      DeleteTemporaryLratImplicationsAfterBacktrack();
     }
 
     // Probing works by taking a series of decisions, and by analyzing what
@@ -1073,6 +1293,7 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
     const int new_level = sat_solver_->CurrentDecisionLevel();
     if (new_level == 0) continue;
     const Literal last_decision = trail_.Decisions()[new_level - 1].literal;
+    binary_clauses_to_extract_.clear();
     for (int i = first_new_trail_index; i < trail_.Index(); ++i) {
       const Literal l = trail_[i];
       if (l == last_decision) continue;
@@ -1096,7 +1317,9 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
         // propagation for one literal we do finish it before calling again
         // the binary propagation.
         if (trail_.AssignmentType(l.Variable()) != binary_propagator_id_) {
-          MaybeExtractImplication(last_decision, l);
+          if (ShouldExtractImplication(l)) {
+            binary_clauses_to_extract_.push_back(l);
+          }
         }
       } else {
         // If we don't extract binary, we don't need to explore any of
@@ -1104,6 +1327,9 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
         processed_.Set(l.Index());
       }
     }
+    if (!binary_clauses_to_extract_.empty()) {
+      ExtractImplications(last_decision, binary_clauses_to_extract_);
+    }
 
     if (options.subsume_with_binary_clause) {
       SubsumeWithBinaryClauseUsingBlockingLiteral(last_decision);
@@ -1112,6 +1338,7 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
 
   if (!sat_solver_->ResetToLevelZero()) return false;
   if (!ProcessLiteralsToFix()) return false;
+  DeleteTemporaryLratImplicationsAfterBacktrack();
   clause_manager_->CleanUpWatchers();
 
   // Display stats.
@@ -1129,6 +1356,8 @@ bool FailedLiteralProbing::DoOneRound(ProbingOptions options) {
       << " explicit_fix:" << num_explicit_fix_
       << " num_conflicts:" << num_conflicts_
       << " new_binary_clauses: " << num_new_binary_
+      << " num_lrat_clauses: " << num_lrat_clauses_
+      << " num_lrat_proof_clauses: " << num_lrat_proof_clauses_
       << " subsumed: " << num_subsumed_ << " dtime: " << time_diff
       << " wtime: " << wall_timer.Get() << (limit_reached ? " (Aborted)" : "");
   return sat_solver_->FinishPropagation();
@@ -1190,8 +1419,10 @@ bool FailedLiteralProbing::ComputeNextDecisionInOrder(
       // This is a backtrack marker, go back one level.
       CHECK_GT(sat_solver_->CurrentDecisionLevel(), 0);
       if (!sat_solver_->BacktrackAndPropagateReimplications(
-              sat_solver_->CurrentDecisionLevel() - 1))
+              sat_solver_->CurrentDecisionLevel() - 1)) {
         return false;
+      }
+      DeleteTemporaryLratImplicationsAfterBacktrack();
       continue;
     }
     const Literal candidate(index);
@@ -1227,6 +1458,7 @@ bool FailedLiteralProbing::GetNextDecisionInNoParticularOrder(
     if (!sat_solver_->BacktrackAndPropagateReimplications(level - 1)) {
       return false;
     }
+    DeleteTemporaryLratImplicationsAfterBacktrack();
   }
   return true;
 }
@@ -1263,6 +1495,7 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
   ClauseId fixed_decision_unit_id = kNoClauseId;
   auto conflict_callback = [&](ClauseId conflict_id,
                                absl::Span<const Literal> conflict_clause) {
+    DeleteTemporaryLratImplicationsAfterBacktrack();
     if (fixed_decision_unit_id != kNoClauseId) return;
     tmp_clause_ids_.clear();
     clause_manager_->AppendClauseIdsFixing(conflict_clause, &tmp_clause_ids_,
@@ -1272,6 +1505,8 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
     lrat_proof_handler_->AddInferredClause(fixed_decision_unit_id,
                                            {Literal(next_decision).Negated()},
                                            tmp_clause_ids_);
+    num_lrat_clauses_++;
+    num_lrat_proof_clauses_ += tmp_clause_ids_.size();
   };
   first_new_trail_index = sat_solver_->EnqueueDecisionAndBackjumpOnConflict(
       Literal(next_decision),
@@ -1282,6 +1517,8 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
   if (first_new_trail_index == kUnsatTrailIndex) return false;
   binary_clause_extracted_.resize(first_new_trail_index);
   binary_clause_extracted_.resize(trail_.Index(), false);
+  trail_implication_clauses_.resize(first_new_trail_index);
+  trail_implication_clauses_.resize(trail_.Index(), {kNoClauseId, false});
 
   // This is tricky, depending on the parameters, and for integer problem,
   // EnqueueDecisionAndBackjumpOnConflict() might create new Booleans.
@@ -1341,15 +1578,19 @@ bool FailedLiteralProbing::EnqueueDecisionAndBackjumpOnConflict(
   return true;
 }
 
-void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
-                                                   const Literal l) {
+bool FailedLiteralProbing::ShouldExtractImplication(const Literal l) {
   const auto& info = trail_.Info(l.Variable());
 
-  if (binary_clause_extracted_[info.trail_index]) return;
+  if (binary_clause_extracted_[info.trail_index]) return false;
   binary_clause_extracted_[info.trail_index] = true;
 
   // If the variable was true at level zero, this is not necessary.
-  if (info.level == 0) return;
+  return info.level > 0;
+}
+
+void FailedLiteralProbing::ExtractImplication(const Literal last_decision,
+                                              const Literal l, bool lrat_only) {
+  const auto& info = trail_.Info(l.Variable());
 
   // TODO(user): Think about trying to extract clause that will not
   // get removed by transitive reduction later. If we can both extract
@@ -1360,7 +1601,6 @@ void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
   // of all literals in the reason for this propagation. And use this
   // as a reason for later hyber binary resolution. Like we do when
   // this clause subsumes the reason.
-  ++num_new_binary_;
   DCHECK(assignment_.LiteralIsTrue(l));
   CHECK_NE(l.Variable(), last_decision.Variable());
 
@@ -1375,19 +1615,97 @@ void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
   if (lrat_proof_handler_ != nullptr) {
     clause_id = clause_id_generator_->GetNextId();
     tmp_clause_ids_.clear();
-    clause_manager_->AppendClauseIdsFixing({l}, &tmp_clause_ids_,
-                                           last_decision);
+    clause_manager_->AppendClauseIdsFixing(
+        {l}, &tmp_clause_ids_, last_decision,
+        [&](int /*level*/, int trail_index) {
+          return trail_implication_clauses_[trail_index].first;
+        });
+    // Cache this LRAT clause so that it can be reused for later proofs. Do this
+    // only if `l` is propagated by the last decision, so that this cache entry
+    // remains valid when we backtrack later decisions.
+    if (info.level == sat_solver_->CurrentDecisionLevel()) {
+      trail_implication_clauses_[info.trail_index] = {clause_id, lrat_only};
+    }
     lrat_proof_handler_->AddInferredClause(
         clause_id, {last_decision.Negated(), l}, tmp_clause_ids_);
+    num_lrat_clauses_++;
+    num_lrat_proof_clauses_ += tmp_clause_ids_.size();
   }
+  if (lrat_only) return;
 
   // Each time we extract a binary clause, we change the reason in the trail.
   // This is important as it will allow us to remove clauses that are now
   // subsumed by this binary, even if it was a reason.
+  ++num_new_binary_;
   CHECK(implication_graph_->AddBinaryClauseAndChangeReason(
       clause_id, l, last_decision.Negated()));
 }
 
+void FailedLiteralProbing::MaybeExtractImplication(const Literal last_decision,
+                                                   const Literal l) {
+  if (ShouldExtractImplication(l)) {
+    ExtractImplication(last_decision, l);
+  }
+}
+
+void FailedLiteralProbing::ExtractImplications(
+    Literal last_decision, absl::Span<const Literal> literals) {
+  // 1. Find all the literals which appear in the expansion of the reasons of
+  //    all the `literals` and collect them in reverse trail order in
+  //    `tmp_marked_literals_`.
+  // 1.a Put the `literals` in a heap.
+  tmp_mark_.ClearAndResize(BooleanVariable(trail_.NumVariables()));
+  tmp_heap_.clear();
+  const VariablesAssignment& assignment = trail_.Assignment();
+  for (const Literal lit : literals) {
+    CHECK(assignment.LiteralIsAssigned(lit));
+    tmp_mark_.Set(lit.Variable());
+    tmp_heap_.push_back(trail_.Info(lit.Variable()).trail_index);
+  }
+  absl::c_make_heap(tmp_heap_);
+
+  // 1.b Expand the reasons of all the literals in the heap and add the reason
+  //     literals back in the heap. Collect the literals in the order they are
+  //     popped from the heap in `tmp_marked_literals_`.
+  tmp_marked_literals_.clear();
+  while (!tmp_heap_.empty()) {
+    absl::c_pop_heap(tmp_heap_);
+    const int trail_index = tmp_heap_.back();
+    tmp_heap_.pop_back();
+    const Literal marked_literal = trail_[trail_index];
+    tmp_marked_literals_.push_back(marked_literal);
+
+    DCHECK_GT(trail_.Info(marked_literal.Variable()).level, 0);
+    DCHECK_NE(trail_.AssignmentType(marked_literal.Variable()),
+              AssignmentType::kSearchDecision);
+
+    for (const Literal literal : trail_.Reason(marked_literal.Variable())) {
+      const BooleanVariable var = literal.Variable();
+      const AssignmentInfo& info = trail_.Info(var);
+      if (info.level > 0 && !tmp_mark_[var] &&
+          trail_.AssignmentType(var) != AssignmentType::kSearchDecision) {
+        tmp_mark_.Set(var);
+        tmp_heap_.push_back(info.trail_index);
+        absl::c_push_heap(tmp_heap_);
+      }
+    }
+  }
+
+  // 2. Add an LRAT implication "last_decision => l" for each literal l in
+  //    `tmp_marked_literals_`, in increasing trail index order. Thanks to the
+  //    cache in ExtractImplication(), the proof for each new implication has
+  //    the same size as its reason. Also add a "real" implication in the binary
+  //    implication graph if `l` is in `literals`.
+  tmp_mark_.ClearAndResize(BooleanVariable(trail_.NumVariables()));
+  for (const Literal lit : literals) {
+    tmp_mark_.Set(lit.Variable());
+  }
+  for (int i = tmp_marked_literals_.size() - 1; i >= 0; --i) {
+    const bool lrat_only = !tmp_mark_[tmp_marked_literals_[i].Variable()];
+    ExtractImplication(last_decision, tmp_marked_literals_[i], lrat_only);
+  }
+}
+
 // If we can extract a binary clause that subsume the reason clause, we do add
 // the binary and remove the subsumed clause.
 //
@@ -1479,6 +1797,8 @@ void FailedLiteralProbing::AddFailedLiteralToFix(const Literal literal) {
   lrat_proof_handler_->AddInferredClause(unit_id, {literal.Negated()},
                                          tmp_clause_ids_);
   to_fix_unit_id_.push_back({unit_id});
+  num_lrat_clauses_++;
+  num_lrat_proof_clauses_ += tmp_clause_ids_.size();
 }
 
 // Fixes all the literals in to_fix_, and finish propagation.
@@ -1498,5 +1818,16 @@ bool FailedLiteralProbing::ProcessLiteralsToFix() {
   return sat_solver_->FinishPropagation();
 }
 
+void FailedLiteralProbing::DeleteTemporaryLratImplicationsAfterBacktrack() {
+  if (lrat_proof_handler_ == nullptr) return;
+  for (int i = trail_.Index(); i < trail_implication_clauses_.size(); ++i) {
+    auto [clause_id, is_temporary] = trail_implication_clauses_[i];
+    if (is_temporary) {
+      lrat_proof_handler_->DeleteClause(clause_id, {});
+    }
+  }
+  trail_implication_clauses_.resize(trail_.Index(), {kNoClauseId, false});
+}
+
 }  // namespace sat
 }  // namespace operations_research
diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h
index 5ef528c409..d42750653d 100644
--- a/ortools/sat/probing.h
+++ b/ortools/sat/probing.h
@@ -43,9 +43,12 @@
 namespace operations_research {
 namespace sat {
 
+class TrailCopy;
+
 class Prober {
  public:
   explicit Prober(Model* model);
+  ~Prober();
 
   // Fixes Booleans variables to true/false and see what is propagated. This
   // can:
@@ -158,6 +161,7 @@ class Prober {
   ClauseManager* clause_manager_;
   ClauseIdGenerator* clause_id_generator_;
   LratProofHandler* lrat_proof_handler_;
+  TrailCopy* trail_copy_;
   const bool drat_enabled_;
 
   // To detect literal x that must be true because b => x and not(b) => x.
@@ -353,9 +357,19 @@ class FailedLiteralProbing {
   // do not contain last_decision.Negated().
   void MaybeSubsumeWithBinaryClause(Literal last_decision, Literal l);
 
-  // If not already done, add last_decision => l to the repository.
+  // Functions to add "last_decision => l" to the repository if not already
+  // done. The Maybe() version just calls Extract() if ShouldExtract() is true.
+  bool ShouldExtractImplication(Literal l);
+  void ExtractImplication(Literal last_decision, Literal l,
+                          bool lrat_only = false);
   void MaybeExtractImplication(Literal last_decision, Literal l);
 
+  // Extracts an implication "`last_decision` => l" for each literal l in
+  // `literals`. This is more efficient than calling ExtractImplication() for
+  // each literal when LRAT is enabled.
+  void ExtractImplications(Literal last_decision,
+                           absl::Span<const Literal> literals);
+
   // Inspect the watcher list for last_decision, If we have a blocking
   // literal at true (implied by last decision), then we have subsumptions.
   //
@@ -375,6 +389,10 @@ class FailedLiteralProbing {
   // Fixes all the literals in to_fix_, and finish propagation.
   bool ProcessLiteralsToFix();
 
+  // Deletes the temporary LRAT clauses in trail_implication_clauses_ for all
+  // trail indices greater than the current trail index.
+  void DeleteTemporaryLratImplicationsAfterBacktrack();
+
   SatSolver* sat_solver_;
   BinaryImplicationGraph* implication_graph_;
   TimeLimit* time_limit_;
@@ -402,13 +420,24 @@ class FailedLiteralProbing {
   std::vector<Literal> to_fix_;
   // For each literal in to_fix_, the ID of the corresponding LRAT unit clause.
   std::vector<ClauseId> to_fix_unit_id_;
+  // The literals for which we want to extract "last_decision => l" clauses.
+  std::vector<Literal> binary_clauses_to_extract_;
 
   // For each literal 'l' in the trail, whether a binary clause "d => l" has
   // been extracted, with 'd' the decision at the same level as 'l'.
   std::vector<bool> binary_clause_extracted_;
 
-  // Temporary vector used for LRAT proofs.
+  // For each literal on the trail, the ID of the LRAT clause stating that this
+  // literal is implied by the previous decisions on the trail (or kNoClauseId
+  // if there is no such clause), plus a Boolean indicating whether this clause
+  // is temporary (i.e., is not an extracted binary clause).
+  std::vector<std::pair<ClauseId, bool>> trail_implication_clauses_;
+
+  // Temporary data structures used for LRAT proofs.
   std::vector<ClauseId> tmp_clause_ids_;
+  SparseBitset<BooleanVariable> tmp_mark_;
+  std::vector<int> tmp_heap_;
+  std::vector<Literal> tmp_marked_literals_;
 
   // Stats.
   int64_t num_probed_ = 0;
@@ -416,6 +445,8 @@ class FailedLiteralProbing {
   int64_t num_conflicts_ = 0;
   int64_t num_new_binary_ = 0;
   int64_t num_subsumed_ = 0;
+  int64_t num_lrat_clauses_ = 0;
+  int64_t num_lrat_proof_clauses_ = 0;
 };
 
 }  // namespace sat
diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py
index 44eab008b8..822dcef220 100644
--- a/ortools/sat/python/cp_model.py
+++ b/ortools/sat/python/cp_model.py
@@ -17,10 +17,10 @@
 The following two sections describe the main
 methods for building and solving CP-SAT models.
 
-* [`CpModel`](#cp_model.CpModel): Methods for creating
-models, including variables and constraints.
-* [`CPSolver`](#cp_model.CpSolver): Methods for solving
-a model and evaluating solutions.
+* [`CpModel`](#cp_model.CpModel): Methods for creating models, including
+  variables and constraints.
+* [`CpSolver`](#cp_model.CpSolver): Methods for solving a model and evaluating
+  solutions.
 
 The following methods implement callbacks that the
 solver calls each time it finds a new solution.
diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc
index d2c85d929c..69769ce84b 100644
--- a/ortools/sat/sat_inprocessing.cc
+++ b/ortools/sat/sat_inprocessing.cc
@@ -15,6 +15,7 @@
 
 #include <algorithm>
 #include <array>
+#include <bitset>
 #include <cmath>
 #include <cstdint>
 #include <deque>
@@ -91,9 +92,21 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) {
 
   // Mainly useful for development.
   double probing_time = 0.0;
-  const bool log_info = VLOG_IS_ON(2);
   const bool log_round_info = VLOG_IS_ON(2);
 
+  // In the presolve, we run this first as some preprocessing technique might
+  // change the problem clauses in such a way that make our heuristic gate
+  // detection miss some gates. Also, when this applies the reduction in problem
+  // size is huge, so it is just faster to run this early.
+  //
+  // TODO(user): If we remove fixed variables, on some problem like:
+  // ~/SAT24/f0426369f61595aee97055965ee7e6a3-hwmcc12miters-xits-iso-6s111.sanitized.cnf.xz
+  // we don't detect as much equivalences... Understand why. I suspect it is due
+  // to the heuristic for ITE gate that combine two clauses of size 3 to get a
+  // truth table on 4 variables. If one of them become of size 2, we might miss
+  // it. Still we should be more robust to stuff like this.
+  RETURN_IF_FALSE(congruence_closure_->DoOneRound(log_round_info));
+
   // We currently do the transformations in a given order and restart each time
   // we did something to make sure that the earlier step cannot strengthen more.
   // This might not be the best, but it is really good during development phase
@@ -159,13 +172,6 @@ bool Inprocessing::PresolveLoop(SatPresolveOptions options) {
       implication_graph_->RemoveAllRedundantVariables(&postsolve_->clauses);
     }
 
-    // TODO(user): Think about the right order in this function.
-    if (params_.inprocessing_use_congruence_closure()) {
-      RETURN_IF_FALSE(RemoveFixedAndEquivalentVariables(log_round_info));
-      RETURN_IF_FALSE(implication_graph_->RemoveDuplicatesAndFixedVariables());
-      RETURN_IF_FALSE(congruence_closure_->DoOneRound(log_info));
-    }
-
     // TODO(user): Combine the two? this way we don't create a full literal <->
     // clause graph twice. It might make sense to reach the BCE fix point which
     // is unique before each variable elimination.
@@ -1974,6 +1980,24 @@ void GateCongruenceClosure::AddToTruthTable(
   }
 }
 
+namespace {
+
+// Given a set of feasible assignment of two variables, recover the
+// corresponding binary clauses.
+void AppendBinaryClausesFromTruthTable(
+    absl::Span<const BooleanVariable> vars, SmallBitset table,
+    std::vector<std::pair<Literal, Literal>>* binary_used) {
+  DCHECK_EQ(vars.size(), 2);
+  for (int b = 0; b < 4; ++b) {
+    if (((table >> b) & 1) == 0) {
+      binary_used->emplace_back(Literal(vars[0], (b & 1) == 0),
+                                Literal(vars[1], (b & 2) == 0));
+    }
+  }
+}
+
+}  // namespace
+
 // Note that this is the "hot" part of the algo, once we have the and gates,
 // the congruence closure should be quite fast.
 void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
@@ -1987,6 +2011,51 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
   tmp_ids_.clear();
   tmp_clauses_.clear();
 
+  // We deal with binary clause a bit differently.
+  //
+  // Tricky: We still include binary clause between fixed literal that haven't
+  // been cleaned up yet, as these are needed to really recover all gates.
+  //
+  // TODO(user): Ideally the detection code should be robust to that.
+  int num_fn1 = 0;
+  std::vector<std::pair<Literal, Literal>> binary_used;
+  for (LiteralIndex a(0); a < implication_graph_->literal_size(); ++a) {
+    if (implication_graph_->IsRedundant(Literal(a))) continue;
+    for (const Literal b : implication_graph_->Implications(Literal(a))) {
+      if (implication_graph_->IsRedundant(b)) continue;
+
+      std::array<BooleanVariable, 2> key2;
+      SmallBitset bitmask;
+      FillKeyAndBitmask({Literal(a).Negated(), b}, absl::MakeSpan(key2),
+                        bitmask);
+      auto [it, inserted] = ids2_.insert({key2, bitmask});
+      if (!inserted) {
+        const SmallBitset old = it->second;
+        it->second &= bitmask;
+        if (it->second != old) {
+          // This is either fixing or equivalence!
+          //
+          // Doing a run of DetectEquivalences() should fix that but then
+          // new clause of size 3 might become binary, and the fix point might
+          // require a lot of step. So it is important to do it here.
+          const SmallBitset bitset2 = it->second;
+          if (lrat_proof_handler_ != nullptr) {
+            binary_used.clear();
+            AppendBinaryClausesFromTruthTable(key2, bitset2, &binary_used);
+          }
+          // If we are equivalent, we always have 2 functions.
+          // But if we fix a variable (like bitset2 = 0011) we just have one.
+          const int num_added =
+              ProcessTruthTable(key2, bitset2, {}, binary_used);
+          CHECK_GE(num_added, 1) << std::bitset<4>(bitset2);
+          num_fn1 += num_added;
+        }
+      }
+    }
+  }
+  timer.AddCounter("t2", ids2_.size());
+  timer.AddCounter("fn1", num_fn1);
+
   std::vector<Literal> candidates;
   for (SatClause* clause : clause_manager_->AllClausesInCreationOrder()) {
     if (timer.WorkLimitIsReached()) break;
@@ -1994,6 +2063,12 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
 
     if (clause->size() == 3) {
       AddToTruthTable<3>(clause, ids3_);
+
+      // The AND gate of size 3 should be detected by the short table code, no
+      // need to do the algo here which should be slower.
+      //
+      // TODO(user): This seems to be less strong. I think we have some bug
+      // in our fixed point loop when we fix variables.
     } else if (clause->size() == 4) {
       AddToTruthTable<4>(clause, ids4_);
     } else if (clause->size() == 5) {
@@ -2065,7 +2140,6 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
       }
     }
 
-    // This relies on having no duplicates.
     for (const Literal target : candidates) {
       if (!(*is_potential_target)[target]) continue;
 
@@ -2089,10 +2163,11 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
       std::swap(is_potential_target, next_is_potential_target);
 
       // Target should imply all other literal in the base clause to false.
-      if (count != clause_size - 1) continue;
+      if (count < clause_size - 1) continue;
 
-      // We have an and_gate !
-      // Double-check no duplicate.
+      // Using only the "count" require that there is no duplicates. But
+      // depending when this is run in the inprocessing loop, we might have
+      // some. Redo a pass to double check.
       int second_count = 0;
       for (const Literal implied : implications) {
         if (implied.Variable() == target.Variable()) continue;
@@ -2101,8 +2176,14 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
           marked_.Clear(implied.Negated());
         }
       }
-      CHECK_EQ(count, second_count);
 
+      // Restore is_clause_literal.
+      for (const Literal l : clause->AsSpan()) {
+        marked_.Set(l);
+      }
+      if (second_count != clause_size - 1) continue;
+
+      // We have an and_gate !
       // Add the detected gate (its inputs are the negation of each clause
       // literal other than the target).
       gates_target_.push_back(target.Index());
@@ -2115,6 +2196,14 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
       }
       if (lrat_proof_handler_ != nullptr) {
         gates_clauses_.Add({clause});
+
+        // Create temporary size 2 clauses for the needed binary.
+        for (const Literal l : clause->AsSpan()) {
+          if (l == target) continue;
+          tmp_binary_clauses_.emplace_back(
+              SatClause::Create({target.Negated(), l.Negated()}));
+          gates_clauses_.AppendToLastVector(tmp_binary_clauses_.back().get());
+        }
       }
 
       // Canonicalize.
@@ -2130,15 +2219,44 @@ void GateCongruenceClosure::ExtractAndGatesAndFillShortTruthTables(
   timer.AddCounter("and_gates", gates_inputs_.size());
 }
 
+int GateCongruenceClosure::CanonicalizeShortGate(GateId id) {
+  // Deals with fixed input variable.
+  absl::Span<LiteralIndex> inputs = gates_inputs_[id];
+  int new_size = inputs.size();
+
+  for (int i = 0; i < new_size;) {
+    if (assignment_.LiteralIsAssigned(Literal(inputs[i]))) {
+      new_size =
+          RemoveFixedInput(i, assignment_.LiteralIsTrue(Literal(inputs[i])),
+                           inputs.subspan(0, new_size), gates_type_[id]);
+    } else {
+      ++i;
+    }
+  }
+
+  // Now canonicalize.
+  new_size = CanonicalizeFunctionTruthTable(
+      gates_target_[id], inputs.subspan(0, new_size), gates_type_[id]);
+
+  // Resize and return.
+  if (new_size < gates_inputs_[id].size()) {
+    gates_inputs_.Shrink(id, new_size);
+  }
+  DCHECK_EQ(gates_type_[id] >> (1 << (gates_inputs_[id].size())), 0);
+  return new_size;
+}
+
 int GateCongruenceClosure::ProcessTruthTable(
     absl::Span<const BooleanVariable> inputs, SmallBitset truth_table,
-    absl::Span<const TruthTableId> ids_for_proof) {
+    absl::Span<const TruthTableId> ids_for_proof,
+    absl::Span<const std::pair<Literal, Literal>> binary_used) {
   int num_detected = 0;
   for (int i = 0; i < inputs.size(); ++i) {
     if (!IsFunction(i, inputs.size(), truth_table)) continue;
     const int num_bits = inputs.size() - 1;
     ++num_detected;
 
+    const GateId new_id(gates_target_.size());
     gates_target_.push_back(Literal(inputs[i], true));
     gates_inputs_.Add({});
     for (int j = 0; j < inputs.size(); ++j) {
@@ -2178,7 +2296,14 @@ int GateCongruenceClosure::ProcessTruthTable(
       for (const TruthTableId id : ids_for_proof) {
         gates_clauses_.AppendToLastVector(truth_tables_clauses_[id]);
       }
+      for (const auto [a, b] : binary_used) {
+        tmp_binary_clauses_.emplace_back(SatClause::Create({a, b}));
+        gates_clauses_.AppendToLastVector(tmp_binary_clauses_.back().get());
+      }
     }
+
+    // Canonicalize right away to deal with corner case.
+    CanonicalizeShortGate(new_id);
   }
   return num_detected;
 }
@@ -2266,6 +2391,44 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
     }
   };
 
+  int num_merges2 = 0;
+  const auto merge2_into_n =
+      [this, &num_merges2](
+          absl::Span<const BooleanVariable> inputs, SmallBitset& truth_table,
+          std::vector<std::pair<Literal, Literal>>& binary_used) {
+        for (int i = 0; i < inputs.size(); ++i) {
+          for (int j = i + 1; j < inputs.size(); ++j) {
+            std::array<BooleanVariable, 2> key2 = {inputs[i], inputs[j]};
+            const auto it = ids2_.find(key2);
+            if (it == ids2_.end()) continue;
+
+            const SmallBitset bitset2 = it->second;
+            SmallBitset bitset = bitset2;
+            int new_size = 0;
+            std::vector<BooleanVariable> key(inputs.size());
+            key[new_size++] = inputs[i];
+            key[new_size++] = inputs[j];
+            for (int t = 0; t < inputs.size(); ++t) {
+              if (t != i && t != j) {
+                key[new_size] = inputs[t];
+                bitset |= bitset << (1 << new_size);  // EXTEND
+                ++new_size;
+              }
+            }
+            CanonicalizeTruthTable<BooleanVariable>(absl::MakeSpan(key),
+                                                    bitset);
+            CHECK_EQ(inputs, absl::MakeSpan(key));
+
+            const SmallBitset old = truth_table;
+            truth_table &= bitset;
+            if (old != truth_table) {
+              AppendBinaryClausesFromTruthTable(key2, bitset2, &binary_used);
+              ++num_merges2;
+            }
+          }
+        }
+      };
+
   // Starts by processing all existing tables.
   //
   // TODO(user): Since we deal with and_gates differently, do we need to look at
@@ -2273,12 +2436,19 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
   // kind of Boolean function on two inputs (and_gates, with any possible
   // negation) and xor_gate.
   std::vector<TruthTableId> ids_for_proof;
+  std::vector<std::pair<Literal, Literal>> binary_used;
   for (TruthTableId t_id(0); t_id < truth_tables_inputs_.size(); ++t_id) {
     ids_for_proof.clear();
     ids_for_proof.push_back(t_id);
     const absl::Span<const BooleanVariable> inputs = truth_tables_inputs_[t_id];
     SmallBitset truth_table = truth_tables_bitset_[t_id];
 
+    // TODO(user): it is unlcear why this is useful. Understand a bit more the
+    // set of possible Boolean functions of 2 and 3 variables and their clause
+    // encoding.
+    binary_used.clear();
+    merge2_into_n(inputs, truth_table, binary_used);
+
     // Merge any size-3 table included inside a size-4 gate.
     // TODO(user): do it for larger gate too ?
     if (inputs.size() == 4) {
@@ -2287,7 +2457,7 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
 
     ++num_tables[inputs.size()];
     const int num_detected =
-        ProcessTruthTable(inputs, truth_table, ids_for_proof);
+        ProcessTruthTable(inputs, truth_table, ids_for_proof, binary_used);
     num_functions[inputs.size() - 1] += num_detected;
 
     // If this is not a function and of size 3, lets try to combine it with
@@ -2344,8 +2514,11 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
           ++num_combinations;
           ++num_tables[4];
           ids_for_proof.clear();
+          binary_used.clear();
+          merge2_into_n(key, bitmask, binary_used);
           merge3_into_4(key, bitmask, ids_for_proof);
-          num_functions[3] += ProcessTruthTable(key, bitmask, ids_for_proof);
+          num_functions[3] +=
+              ProcessTruthTable(key, bitmask, ids_for_proof, binary_used);
         }
       }
     }
@@ -2353,12 +2526,13 @@ void GateCongruenceClosure::ExtractShortGates(PresolveTimer& timer) {
 
   timer.AddCounter("combine3", num_combinations);
   timer.AddCounter("merges", num_merges);
+  timer.AddCounter("merges2", num_merges2);
 
   // Note that we only display non-zero counters.
-  for (int i = 2; i < num_tables.size(); ++i) {
+  for (int i = 0; i < num_tables.size(); ++i) {
     timer.AddCounter(absl::StrCat("t", i), num_tables[i]);
   }
-  for (int i = 2; i < num_functions.size(); ++i) {
+  for (int i = 0; i < num_functions.size(); ++i) {
     timer.AddCounter(absl::StrCat("fn", i), num_functions[i]);
   }
 }
@@ -2368,13 +2542,14 @@ namespace {
 class LratGateCongruenceHelper {
  public:
   LratGateCongruenceHelper(
-      const BinaryImplicationGraph* implication_graph,
+      const Trail* trail, const BinaryImplicationGraph* implication_graph,
       ClauseManager* clause_manager, ClauseIdGenerator* clause_id_generator,
       LratProofHandler* lrat_proof_handler,
       const util_intops::StrongVector<GateId, LiteralIndex>& gates_target,
       const CompactVectorVector<GateId, const SatClause*>& gates_clauses,
       DenseConnectedComponentsFinder& union_find)
-      : implication_graph_(implication_graph),
+      : trail_(trail),
+        implication_graph_(implication_graph),
         clause_manager_(clause_manager),
         clause_id_generator_(clause_id_generator),
         lrat_proof_handler_(lrat_proof_handler),
@@ -2519,6 +2694,8 @@ class LratGateCongruenceHelper {
 
   void AddGateClausesToTemporaryProof(GateId id) {
     CHECK(lrat_proof_handler_ != nullptr);
+    const auto& assignment = trail_->Assignment();
+    std::vector<Literal> fixed;
     for (const SatClause* clause : gates_clauses_[id]) {
       // We rewrite each clause using new equivalences found.
       marked_.ResetAllToFalse();
@@ -2528,6 +2705,9 @@ class LratGateCongruenceHelper {
       bool some_change = false;
       for (const Literal lit : clause->AsSpan()) {
         const Literal rep = GetRepresentativeWithProofSupport(lit);
+        if (assignment.LiteralIsAssigned(rep)) {
+          fixed.push_back(rep);
+        }
         if (rep != lit) {
           some_change = true;
           // We need not(rep) => not(lit). This should be equivalent to
@@ -2547,7 +2727,12 @@ class LratGateCongruenceHelper {
       // If this is the case, we shouldn't need it for the proof.
       if (clause_is_trivial) continue;
 
-      ClauseId new_id = clause_manager_->GetClauseId(clause);
+      ClauseId new_id =
+          clause->size() == 2
+              ? implication_graph_->GetClauseId(clause->FirstLiteral(),
+                                                clause->SecondLiteral())
+              : clause_manager_->GetClauseId(clause);
+      CHECK_NE(new_id, kNoClauseId);
       if (some_change) {
         // If there is some change, we add a temporary clause id with the
         // proof to go from the original clause to this one.
@@ -2563,81 +2748,32 @@ class LratGateCongruenceHelper {
       tmp_proof_clauses_.Add(tmp_literals_);
     }
 
-    // Hacky: If we have a single clause, then there is a chance this was
-    // an and_gate. We must add all the implications target => inputs[i].
-    // Note that the inputs are the negation of the literals in the unique
-    // clause, so we really have target => not(lit) for lit in clause.
-    // which gives (not(target), not(lit)) for the needed clause.
-    if (gates_clauses_[id].size() == 1) {
-      // Tricky: The target might have been negated ! so we recover it from
-      // the unique clause.
-      const Literal current = Literal(gates_target_[id]);
-      LiteralIndex real_target = kNoLiteralIndex;
-      for (const Literal lit : gates_clauses_[id][0]->AsSpan()) {
-        if (current.Variable() == lit.Variable()) {
-          real_target = lit.Index();
-        }
-      }
-      if (real_target == kNoLiteralIndex) return;
-
-      const Literal neg_target = Literal(real_target).Negated();
-      const Literal neg_target_rep =
-          GetRepresentativeWithProofSupport(neg_target);
-      for (const Literal lit : gates_clauses_[id][0]->AsSpan()) {
-        const Literal neg_lit = lit.Negated();
-        if (neg_lit == neg_target) continue;
-
-        // Skip trivial clause after rewrite.
-        const Literal neg_lit_rep = GetRepresentativeWithProofSupport(neg_lit);
-        if (neg_lit_rep == neg_target_rep.Negated()) continue;
-
-        ClauseId new_id = implication_graph_->GetClauseId(neg_target, neg_lit);
-        if (new_id == kNoClauseId) {
-          // We where likely not a bool_and to start with, so we shouldn't need
-          // these clauses.
-          break;
-        }
-
-        if (neg_lit != neg_lit_rep || neg_target != neg_target_rep) {
-          tmp_clause_ids_.clear();
-          tmp_index_to_delete_.push_back(tmp_proof_clauses_.size());
-          if (neg_lit != neg_lit_rep) {
-            tmp_clause_ids_.push_back(
-                GetLiteralImpliesRepresentativeClauseId(neg_lit));
-          }
-          if (neg_target != neg_target_rep) {
-            tmp_clause_ids_.push_back(
-                GetLiteralImpliesRepresentativeClauseId(neg_target));
-          }
-          tmp_clause_ids_.push_back(new_id);
-
-          new_id = clause_id_generator_->GetNextId();
-          lrat_proof_handler_->AddInferredClause(
-              new_id, {neg_target_rep, neg_lit_rep}, tmp_clause_ids_);
-        }
-
-        tmp_proof_clauses_id_.push_back(new_id);
-        CHECK_NE(neg_target_rep, neg_lit_rep);
-        tmp_proof_clauses_.Add({neg_target_rep, neg_lit_rep});
+    // Add size1 clauses.
+    gtl::STLSortAndRemoveDuplicates(&fixed);
+    for (const Literal lit : fixed) {
+      if (assignment.LiteralIsAssigned(lit)) {
+        tmp_proof_clauses_id_.push_back(
+            trail_->GetUnitClauseId(lit.Variable()));
+        tmp_proof_clauses_.Add(
+            {assignment.LiteralIsTrue(lit) ? lit : lit.Negated()});
       }
     }
   }
 
   // Same as AddAndGateTargetImplication() but with truth table based gates.
-  std::pair<ClauseId, ClauseId> AddShortGateTargetEquivalence(
-      GateId gate_a_id, GateId gate_b_id) {
+  std::pair<ClauseId, ClauseId> AddShortGateEquivalence(
+      Literal rep_a, Literal rep_b, absl::Span<const GateId> gate_ids) {
+    if (lrat_proof_handler_ == nullptr) return {kNoClauseId, kNoClauseId};
+
     // Just add all clauses from both gates.
     // But note that we need to remap them.
     ClearTemporaryProof();
-    AddGateClausesToTemporaryProof(gate_a_id);
-    AddGateClausesToTemporaryProof(gate_b_id);
+    for (const GateId id : gate_ids) {
+      AddGateClausesToTemporaryProof(id);
+    }
 
     // All clauses are now in tmp_proof_clauses_/tmp_proof_clauses_id_.
     // We can add both implications with proof.
-    const Literal a = Literal(gates_target_[gate_a_id]);
-    const Literal b = Literal(gates_target_[gate_b_id]);
-    const Literal rep_a = GetRepresentativeWithProofSupport(a);
-    const Literal rep_b = GetRepresentativeWithProofSupport(b);
     DCHECK(IsRepresentative(rep_a));
     DCHECK(IsRepresentative(rep_b));
     CHECK_NE(rep_a, rep_b);
@@ -2677,6 +2813,7 @@ class LratGateCongruenceHelper {
   }
 
   ClauseId ProofForFixingLiteral(Literal to_fix, GateId id) {
+    if (lrat_proof_handler_ == nullptr) return kNoClauseId;
     CHECK(IsRepresentative(to_fix));
     ClearTemporaryProof();
     AddGateClausesToTemporaryProof(id);
@@ -2766,6 +2903,7 @@ class LratGateCongruenceHelper {
     }
   }
 
+  const Trail* trail_;
   const BinaryImplicationGraph* implication_graph_;
   ClauseManager* clause_manager_;
   ClauseIdGenerator* clause_id_generator_;
@@ -2815,6 +2953,10 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
   gates_type_.clear();
   gates_clauses_.clear();
 
+  // Lets release the memory on exit.
+  CHECK(tmp_binary_clauses_.empty());
+  absl::Cleanup cleanup = [this] { tmp_binary_clauses_.clear(); };
+
   ExtractAndGatesAndFillShortTruthTables(timer);
   ExtractShortGates(timer);
 
@@ -2847,7 +2989,7 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
   input_literals_to_gate.ResetFromTranspose(gates_inputs_, num_literals);
 
   LratGateCongruenceHelper lrat_helper(
-      implication_graph_, clause_manager_, clause_id_generator_,
+      trail_, implication_graph_, clause_manager_, clause_id_generator_,
       lrat_proof_handler_, gates_target_, gates_clauses_, union_find);
 
   // Starts with all gates in the queue.
@@ -2856,10 +2998,108 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
   std::vector<GateId> queue(num_gates);
   for (GateId id(0); id < num_gates; ++id) queue[id.value()] = id;
 
-  // Main loop.
   int num_units = 0;
-  int num_processed = 0;
+  const auto fix_literal = [&, this](Literal to_fix,
+                                     absl::Span<const ClauseId> clause_ids) {
+    if (assignment_.LiteralIsTrue(to_fix)) return true;
+    if (!clause_manager_->InprocessingFixLiteral(to_fix, clause_ids)) {
+      return false;
+    }
+
+    ++num_units;
+    for (const GateId gate_id : input_literals_to_gate[to_fix]) {
+      if (in_queue[gate_id.value()]) continue;
+      queue.push_back(gate_id);
+      in_queue[gate_id.value()] = true;
+    }
+    for (const GateId gate_id : input_literals_to_gate[to_fix.Negated()]) {
+      if (in_queue[gate_id.value()]) continue;
+      queue.push_back(gate_id);
+      in_queue[gate_id.value()] = true;
+    }
+    return true;
+  };
+
+  const auto get_unit_clause = [this](Literal a) {
+    if (lrat_proof_handler_ == nullptr) return kNoClauseId;
+    return trail_->GetUnitClauseId(a.Variable());
+  };
+
   int num_equivalences = 0;
+  const auto new_equivalence = [&, this](Literal a, Literal b,
+                                         ClauseId a_implies_b,
+                                         ClauseId b_implies_a) {
+    // Lets propagate fixed variable as we find new equivalences.
+    if (assignment_.LiteralIsAssigned(a)) {
+      if (assignment_.LiteralIsTrue(a)) {
+        return fix_literal(b, {a_implies_b, get_unit_clause(a)});
+      } else {
+        return fix_literal(b.Negated(), {b_implies_a, get_unit_clause(a)});
+      }
+    } else if (assignment_.LiteralIsAssigned(b)) {
+      if (assignment_.LiteralIsTrue(b)) {
+        return fix_literal(a, {b_implies_a, get_unit_clause(b)});
+      } else {
+        return fix_literal(a.Negated(), {a_implies_b, get_unit_clause(b)});
+      }
+    }
+
+    ++num_equivalences;
+    DCHECK(!implication_graph_->IsRedundant(a));
+    DCHECK(!implication_graph_->IsRedundant(b));
+    if (!implication_graph_->AddBinaryClause(a_implies_b, a.Negated(), b) ||
+        !implication_graph_->AddBinaryClause(b_implies_a, b.Negated(), a)) {
+      return false;
+    }
+
+    for (const bool negate : {false, true}) {
+      const LiteralIndex x = negate ? a.NegatedIndex() : a.Index();
+      const LiteralIndex y = negate ? b.NegatedIndex() : b.Index();
+      const ClauseId x_implies_y = negate ? b_implies_a : a_implies_b;
+      const ClauseId y_implies_x = negate ? a_implies_b : b_implies_a;
+
+      // Because x always refer to a and y to b, this should maintain
+      // the invariant root(lit) = root(lit.Negated()).Negated().
+      // This is checked below.
+      union_find.AddEdge(x.value(), y.value());
+      const LiteralIndex rep(union_find.FindRoot(y.value()));
+      const LiteralIndex to_merge = rep == x ? y : x;
+      input_literals_to_gate.MergeInto(to_merge, rep);
+
+      if (lrat_proof_handler_ != nullptr) {
+        if (rep == x) {
+          lrat_helper.AddGateEquivalenceClauses(Literal(y), y_implies_x,
+                                                x_implies_y);
+        } else {
+          lrat_helper.AddGateEquivalenceClauses(Literal(x), x_implies_y,
+                                                y_implies_x);
+        }
+      }
+
+      // Re-add to the queue all gates with touched inputs.
+      //
+      // TODO(user): I think we could only add the gates of "to_merge"
+      // before we merge. This part of the code is quite quick in any
+      // case.
+      for (const GateId gate_id : input_literals_to_gate[rep]) {
+        if (in_queue[gate_id.value()]) continue;
+        queue.push_back(gate_id);
+        in_queue[gate_id.value()] = true;
+      }
+    }
+
+    // Invariant.
+    CHECK_EQ(
+        lrat_helper.GetRepresentativeWithProofSupport(a),
+        lrat_helper.GetRepresentativeWithProofSupport(a.Negated()).Negated());
+    CHECK_EQ(
+        lrat_helper.GetRepresentativeWithProofSupport(b),
+        lrat_helper.GetRepresentativeWithProofSupport(b.Negated()).Negated());
+    return true;
+  };
+
+  // Main loop.
+  int num_processed = 0;
   int arity1_equivalences = 0;
   while (!queue.empty()) {
     ++num_processed;
@@ -2912,7 +3152,6 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
         const Literal rep_b = lrat_helper.GetRepresentativeWithProofSupport(b);
 
         if (rep_a != rep_b) {
-          ++num_equivalences;
           ClauseId rep_a_implies_rep_b = kNoClauseId;
           ClauseId rep_b_implies_rep_a = kNoClauseId;
           if (lrat_proof_handler_ != nullptr) {
@@ -2922,71 +3161,16 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
               rep_b_implies_rep_a =
                   lrat_helper.AddAndGateTargetImplication(other_id, id);
             } else {
-              const auto [x, y] =
-                  lrat_helper.AddShortGateTargetEquivalence(id, other_id);
+              const auto [x, y] = lrat_helper.AddShortGateEquivalence(
+                  rep_a, rep_b, {id, other_id});
               rep_a_implies_rep_b = x;
               rep_b_implies_rep_a = y;
             }
           }
-
-          DCHECK(!implication_graph_->IsRedundant(rep_a));
-          DCHECK(!implication_graph_->IsRedundant(rep_b));
-          if (!implication_graph_->AddBinaryClause(rep_a_implies_rep_b,
-                                                   rep_a.Negated(), rep_b) ||
-              !implication_graph_->AddBinaryClause(rep_b_implies_rep_a,
-                                                   rep_b.Negated(), rep_a)) {
+          if (!new_equivalence(rep_a, rep_b, rep_a_implies_rep_b,
+                               rep_b_implies_rep_a)) {
             return false;
           }
-
-          for (const bool negate : {false, true}) {
-            const LiteralIndex x =
-                negate ? rep_a.NegatedIndex() : rep_a.Index();
-            const LiteralIndex y =
-                negate ? rep_b.NegatedIndex() : rep_b.Index();
-            const ClauseId x_implies_y =
-                negate ? rep_b_implies_rep_a : rep_a_implies_rep_b;
-            const ClauseId y_implies_x =
-                negate ? rep_a_implies_rep_b : rep_b_implies_rep_a;
-
-            // Because x always refer to a and y to b, this should maintain
-            // the invariant root(lit) = root(lit.Negated()).Negated().
-            // This is checked below.
-            union_find.AddEdge(x.value(), y.value());
-            const LiteralIndex rep(union_find.FindRoot(y.value()));
-            const LiteralIndex to_merge = rep == x ? y : x;
-            input_literals_to_gate.MergeInto(to_merge, rep);
-
-            if (lrat_proof_handler_ != nullptr) {
-              if (rep == x) {
-                lrat_helper.AddGateEquivalenceClauses(Literal(y), y_implies_x,
-                                                      x_implies_y);
-              } else {
-                lrat_helper.AddGateEquivalenceClauses(Literal(x), x_implies_y,
-                                                      y_implies_x);
-              }
-            }
-
-            // Re-add to the queue all gates with touched inputs.
-            //
-            // TODO(user): I think we could only add the gates of "to_merge"
-            // before we merge. This part of the code is quite quick in any
-            // case.
-            for (const GateId gate_id : input_literals_to_gate[rep]) {
-              if (in_queue[gate_id.value()]) continue;
-              queue.push_back(gate_id);
-              in_queue[gate_id.value()] = true;
-            }
-          }
-
-          // Invariant.
-          CHECK_EQ(
-              lrat_helper.GetRepresentativeWithProofSupport(rep_a),
-              lrat_helper.GetRepresentativeWithProofSupport(rep_a.Negated())
-                  .Negated());
-          CHECK_EQ(
-              lrat_helper.GetRepresentativeWithProofSupport(rep_b),
-              lrat_helper.GetRepresentativeWithProofSupport(rep_b.Negated())
-                  .Negated());
         }
         break;
       }
@@ -3016,6 +3200,8 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
           // then target must be false.
           if (marked_[Literal(rep).Negated()]) {
             is_unit = true;
+            input_literals_to_gate.RemoveFromFutureOutput(id);
+
             const Literal to_fix = Literal(gates_target_[id]).Negated();
             if (!assignment_.LiteralIsTrue(to_fix)) {
               absl::InlinedVector<ClauseId, 4> clause_ids;
@@ -3023,10 +3209,7 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
                 lrat_helper.AppendFixAndGateTargetClauses(id, Literal(rep),
                                                           clause_ids);
               }
-              if (!clause_manager_->InprocessingFixLiteral(to_fix,
-                                                           clause_ids)) {
-                return false;
-              }
+              if (!fix_literal(to_fix, clause_ids)) return false;
             }
             break;
           }
@@ -3036,8 +3219,6 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
         }
 
         if (is_unit) {
-          ++num_units;
-          input_literals_to_gate.RemoveFromFutureOutput(id);
           break;  // Abort the passes loop.
         }
 
@@ -3077,43 +3258,36 @@ bool GateCongruenceClosure::DoOneRound(bool log_info) {
                 .Index();
       }
 
-      const int new_size = CanonicalizeFunctionTruthTable(
-          gates_target_[id], inputs, gates_type_[id]);
-      if (new_size < inputs.size()) {
-        gates_inputs_.Shrink(id, new_size);
-      }
-      DCHECK_EQ(gates_type_[id] >> (1 << (inputs.size())), 0);
-
+      const int new_size = CanonicalizeShortGate(id);
       if (new_size == 1) {
         // We have a function of size 1! This is an equivalence.
-        //
-        // TODO(user): deal with it.
-        ++arity1_equivalences;
         input_literals_to_gate.RemoveFromFutureOutput(id);
+        const Literal a = Literal(gates_target_[id]);
+        const Literal b = Literal(gates_inputs_[id][0]);
+        const Literal rep_a = lrat_helper.GetRepresentativeWithProofSupport(a);
+        const Literal rep_b = lrat_helper.GetRepresentativeWithProofSupport(b);
+        if (rep_a != rep_b) {
+          ++arity1_equivalences;
+          const auto [a_to_b, b_to_a] =
+              lrat_helper.AddShortGateEquivalence(rep_a, rep_b, {id});
+          if (!new_equivalence(rep_a, rep_b, a_to_b, b_to_a)) {
+            return false;
+          }
+        }
         break;
       } else if (new_size == 0) {
         // We have a fixed function! Just fix the literal.
+        input_literals_to_gate.RemoveFromFutureOutput(id);
         const Literal initial_to_fix =
             (gates_type_[id] & 1) == 1 ? Literal(gates_target_[id])
                                        : Literal(gates_target_[id]).Negated();
         const Literal to_fix =
             lrat_helper.GetRepresentativeWithProofSupport(initial_to_fix);
         if (!assignment_.LiteralIsTrue(to_fix)) {
-          if (lrat_proof_handler_ == nullptr) {
-            if (!clause_manager_->InprocessingFixLiteral(to_fix, {})) {
-              return false;
-            }
-          } else {
-            const ClauseId clause_id =
-                lrat_helper.ProofForFixingLiteral(to_fix, id);
-            if (!clause_manager_->InprocessingAddUnitClause(clause_id,
-                                                            to_fix)) {
-              return false;
-            }
-          }
-          ++num_units;
+          const ClauseId clause_id =
+              lrat_helper.ProofForFixingLiteral(to_fix, id);
+          if (!fix_literal(to_fix, {clause_id})) return false;
         }
-        input_literals_to_gate.RemoveFromFutureOutput(id);
         break;
       }
     }
diff --git a/ortools/sat/sat_inprocessing.h b/ortools/sat/sat_inprocessing.h
index a3c3d21848..488457e44f 100644
--- a/ortools/sat/sat_inprocessing.h
+++ b/ortools/sat/sat_inprocessing.h
@@ -449,6 +449,7 @@ class GateCongruenceClosure {
   explicit GateCongruenceClosure(Model* model)
       : assignment_(model->GetOrCreate<Trail>()->Assignment()),
         sat_solver_(model->GetOrCreate<SatSolver>()),
+        trail_(model->GetOrCreate<Trail>()),
         implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
         clause_manager_(model->GetOrCreate<ClauseManager>()),
         clause_id_generator_(model->GetOrCreate<ClauseIdGenerator>()),
@@ -508,9 +509,10 @@ class GateCongruenceClosure {
 
   // Detects gates encoded in the given truth table, and add them to the set
   // of gates. Returns the number of gate detected.
-  int ProcessTruthTable(absl::Span<const BooleanVariable> inputs,
-                        SmallBitset truth_table,
-                        absl::Span<const TruthTableId> ids_for_proof = {});
+  int ProcessTruthTable(
+      absl::Span<const BooleanVariable> inputs, SmallBitset truth_table,
+      absl::Span<const TruthTableId> ids_for_proof,
+      absl::Span<const std::pair<Literal, Literal>> binary_used);
 
   // Add a small clause to the corresponding truth table.
   template <int arity>
@@ -518,8 +520,13 @@ class GateCongruenceClosure {
                        absl::flat_hash_map<std::array<BooleanVariable, arity>,
                                            TruthTableId>& ids);
 
+  // Make sure the small gate at given id is canonicalized.
+  // Returns its number of inputs.
+  int CanonicalizeShortGate(GateId id);
+
   const VariablesAssignment& assignment_;
   SatSolver* sat_solver_;
+  Trail* trail_;
   BinaryImplicationGraph* implication_graph_;
   ClauseManager* clause_manager_;
   ClauseIdGenerator* clause_id_generator_;
@@ -554,6 +561,14 @@ class GateCongruenceClosure {
   CompactVectorVector<GateId, LiteralIndex> gates_inputs_;
   CompactVectorVector<GateId, const SatClause*> gates_clauses_;
 
+  // Truth tables on 2 variables are handled differently, and we don't use
+  // a TruthTableId indirection.
+  //
+  // TODO(user): it feels like we could benefit from just storing this all
+  // the time in the binary_implication graph. This allow to never add duplicate
+  // and detect easy case of fixing/equivalences right away. To investigate.
+  absl::flat_hash_map<std::array<BooleanVariable, 2>, SmallBitset> ids2_;
+
   // Map (Xi) (sorted) to a bitmask corresponding to the allowed values.
   // We loop over all short clauses to fill this. We actually store an "id"
   // pointing in the vectors below.
@@ -571,6 +586,10 @@ class GateCongruenceClosure {
   std::vector<TruthTableId> tmp_ids_;
   std::vector<SatClause*> tmp_clauses_;
 
+  // Temporary SatClause* for binary, so we don't need to specialize too much
+  // code for them.
+  std::vector<std::unique_ptr<SatClause>> tmp_binary_clauses_;
+
   // For stats.
   double total_dtime_ = 0.0;
   double total_wtime_ = 0.0;
diff --git a/ortools/sat/scheduling_helpers.cc b/ortools/sat/scheduling_helpers.cc
index 6ae244be5c..c5ff549492 100644
--- a/ortools/sat/scheduling_helpers.cc
+++ b/ortools/sat/scheduling_helpers.cc
@@ -531,6 +531,17 @@ void SchedulingConstraintHelper::AddReasonForBeingBeforeAssumingNoOverlap(
                           starts_[before].var == ends_[before].var &&
                           starts_[after].var == ends_[after].var;
 
+  if (fixed_size && sizes_[after].constant == 0 &&
+      sizes_[before].constant == 0) {
+    // If both sizes are fixed to zero use the trivial explanation.
+    const auto [expr, ub] =
+        EncodeDifferenceLowerThan(ends_[before], starts_[after], 0);
+    DCHECK_LE(linear2_bounds_->UpperBound(expr), ub);
+    linear2_bounds_->AddReasonForUpperBoundLowerThan(expr, ub, &literal_reason_,
+                                                     &integer_reason_);
+    return;
+  }
+
   // Prefer the straightforward linear2 explanation as it is more likely this
   // comes from level zero or a single enforcement literal. Also handle the
   // fixed size case. This explains with at most two integer bounds.