(proof-new) Implements the conversion between EqProof and ProofNode (#4756)

2 files changed, 1169 insertions, 5 deletions

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 3a60d246e..70edbd0dd 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -86,7 +86,31 @@ void EqProof::debug_print(std::ostream& os,
   os << ")" << std::endl;
 }
 
-void EqProof::cleanReflPremises(std::vector<Node>& premises) const {}
+void EqProof::cleanReflPremises(std::vector<Node>& premises) const
+{
+  std::vector<Node> newPremises;
+  unsigned size = premises.size();
+  for (unsigned i = 0; i < size; ++i)
+  {
+    if (premises[i][0] == premises[i][1])
+    {
+      continue;
+    }
+    newPremises.push_back(premises[i]);
+  }
+  if (newPremises.size() != size)
+  {
+    Trace("eqproof-conv") << "EqProof::cleanReflPremises: removed "
+                          << (newPremises.size() >= size
+                                  ? newPremises.size() - size
+                                  : 0)
+                          << " refl premises from " << premises << "\n";
+    premises.clear();
+    premises.insert(premises.end(), newPremises.begin(), newPremises.end());
+    Trace("eqproof-conv") << "EqProof::cleanReflPremises: new premises "
+                          << premises << "\n";
+  }
+}
 
 bool EqProof::expandTransitivityForDisequalities(
     Node conclusion,
@@ -94,12 +118,492 @@ bool EqProof::expandTransitivityForDisequalities(
     CDProof* p,
     std::unordered_set<Node, NodeHashFunction>& assumptions) const
 {
-  return false;
+  Trace("eqproof-conv")
+      << "EqProof::expandTransitivityForDisequalities: check if need "
+         "to expand transitivity step to conclude "
+      << conclusion << " from premises " << premises << "\n";
+  // Check premises to see if any of the form (= (= t1 t2) false), modulo
+  // symmetry
+  unsigned size = premises.size();
+  // termPos is, in (= (= t1 t2) false) or (= false (= t1 t2)), the position of
+  // the equality. When the i-th premise has that form, offending = i
+  unsigned termPos = 2, offending = size;
+  for (unsigned i = 0; i < size; ++i)
+  {
+    Assert(premises[i].getKind() == kind::EQUAL);
+    for (unsigned j = 0; j < 2; ++j)
+    {
+      if (premises[i][j].getKind() == kind::CONST_BOOLEAN
+          && !premises[i][j].getConst<bool>()
+          && premises[i][1 - j].getKind() == kind::EQUAL)
+      {
+        // there is only one offending equality
+        Assert(offending == size);
+        offending = i;
+        termPos = 1 - j;
+        break;
+      }
+    }
+  }
+  // if no equality of the searched form, nothing to do
+  if (offending == size)
+  {
+    return false;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(termPos == 0 || termPos == 1);
+  Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found "
+                           "offending equality at index "
+                        << offending << " : " << premises[offending] << "\n";
+  // collect the premises to be used in the expansion, which are all but the
+  // offending one
+  std::vector<Node> expansionPremises;
+  for (unsigned i = 0; i < size; ++i)
+  {
+    if (i != offending)
+    {
+      expansionPremises.push_back(premises[i]);
+    }
+  }
+  // Eliminate spurious premises. Reasoning below assumes no refl steps.
+  cleanReflPremises(expansionPremises);
+  Assert(!expansionPremises.empty());
+  // Check if we are in the substitution case
+  Node expansionConclusion;
+  std::vector<Node> substPremises;
+  bool inSubstCase = false, substConclusionInReverseOrder = false;
+  if ((conclusion[0].getKind() == kind::CONST_BOOLEAN)
+      != (conclusion[1].getKind() == kind::CONST_BOOLEAN))
+  {
+    inSubstCase = true;
+    // reorder offending premise if constant is the first argument
+    if (termPos == 1)
+    {
+      premises[offending] =
+          premises[offending][1].eqNode(premises[offending][0]);
+    }
+    // reorder conclusion if constant is the first argument
+    conclusion = conclusion[1].getKind() == kind::CONST_BOOLEAN
+                     ? conclusion
+                     : conclusion[1].eqNode(conclusion[0]);
+    // equality term in premise disequality
+    Node premiseTermEq = premises[offending][0];
+    // equality term in conclusion disequality
+    Node conclusionTermEq = conclusion[0];
+    Trace("eqproof-conv")
+        << "EqProof::expandTransitivityForDisequalities: Substitition "
+           "case. Need to build subst from "
+        << premiseTermEq << " to " << conclusionTermEq << "\n";
+    // If only one argument in the premise is substituted, premiseTermEq and
+    // conclusionTermEq will share one argument and the other argument change
+    // defines the single substitution. Otherwise both arguments are replaced,
+    // so there are two substitutions.
+    std::vector<Node> subs[2];
+    subs[0].push_back(premiseTermEq[0]);
+    subs[1].push_back(premiseTermEq[1]);
+    // which of the arguments of premiseTermEq, if any, is equal to one argument
+    // of conclusionTermEq
+    int equalArg = -1;
+    for (unsigned i = 0; i < 2; ++i)
+    {
+      for (unsigned j = 0; j < 2; ++j)
+      {
+        if (premiseTermEq[i] == conclusionTermEq[j])
+        {
+          equalArg = i;
+          // identity sub
+          subs[i].push_back(conclusionTermEq[j]);
+          // sub that changes argument
+          subs[1 - i].push_back(conclusionTermEq[1 - j]);
+          // wither e.g. (= t1 t2), with sub t1->t3, becomes (= t2 t3)
+          substConclusionInReverseOrder = i != j;
+          break;
+        }
+      }
+    }
+    // simple case of single substitution
+    if (equalArg >= 0)
+    {
+      // case of
+      //   (= (= t1 t2) false) (= t1 x1) ... (= xn t3)
+      //  -------------------------------------------- EQP::TR
+      //          (= (= t3 t2) false)
+      // where
+      //
+      //   (= t1 x1) ... (= xn t3)           - expansion premises
+      //  ------------------------ TRANS
+      //          (= t1 t3)                  - expansion conclusion
+      //
+      // will be the expansion made to justify the substitution for t1->t3.
+      expansionConclusion = subs[1 - equalArg][0].eqNode(subs[1 - equalArg][1]);
+      Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
+                               "Need to expand premises into "
+                            << expansionConclusion << "\n";
+      // add refl step for the substitition t2->t2
+      p->addStep(subs[equalArg][0].eqNode(subs[equalArg][1]),
+                 PfRule::REFL,
+                 {},
+                 {subs[equalArg][0]});
+    }
+    else
+    {
+      // Hard case. We determine, and justify, the substitutions t1->t3/t4 and
+      // t2->t3/t4 based on the expansion premises.
+      Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
+                               "Need two substitutions. Look for "
+                            << premiseTermEq[0] << " and " << premiseTermEq[1]
+                            << " in premises " << expansionPremises << "\n";
+      Assert(expansionPremises.size() >= 2)
+          << "Less than 2 expansion premises for substituting BOTH terms in "
+             "disequality.\nDisequality: "
+          << premises[offending]
+          << "\nExpansion premises: " << expansionPremises
+          << "\nConclusion: " << conclusion << "\n";
+      // Easier case where we can determine the substitutions by directly
+      // looking at the premises, i.e. the two expansion premises are for
+      // example (= t1 t3) and (= t2 t4)
+      if (expansionPremises.size() == 2)
+      {
+        // iterate over args to be substituted
+        for (unsigned i = 0; i < 2; ++i)
+        {
+          // iterate over premises
+          for (unsigned j = 0; j < 2; ++j)
+          {
+            // iterate over args in premise
+            for (unsigned k = 0; k < 2; ++k)
+            {
+              if (premiseTermEq[i] == expansionPremises[j][k])
+              {
+                subs[i].push_back(expansionPremises[j][1 - k]);
+                break;
+              }
+            }
+          }
+          Assert(subs[i].size() == 2)
+              << " did not find term " << subs[i][0] << "\n";
+          // check if argument to be substituted is in the same order in the
+          // conclusion
+          substConclusionInReverseOrder =
+              premiseTermEq[i] != conclusionTermEq[i];
+        }
+      }
+      else
+      {
+        Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
+                                 "Build transitivity chains "
+                                 "for two subs among more than 2 premises: "
+                              << expansionPremises << "\n";
+        // Hardest case. Try building a transitivity chain for (= t1 t3). If it
+        // can be built, use the remaining expansion premises to build a chain
+        // for (= t2 t4). Otherwise build it for (= t1 t4) and then build it for
+        // (= t2 t3). It should always succeed.
+        subs[0].push_back(conclusionTermEq[0]);
+        subs[1].push_back(conclusionTermEq[1]);
+        for (unsigned i = 0; i < 2; ++i)
+        {
+          // copy premises, since buildTransitivityChain is destructive
+          std::vector<Node> copy1ofExpPremises(expansionPremises.begin(),
+                                               expansionPremises.end());
+          Node transConclusion1 = subs[0][0].eqNode(subs[0][1]);
+          if (!buildTransitivityChain(transConclusion1, copy1ofExpPremises))
+          {
+            AlwaysAssert(i == 0)
+                << "Couldn't find sub at all for substituting BOTH terms in "
+                   "disequality.\nDisequality: "
+                << premises[offending]
+                << "\nExpansion premises: " << expansionPremises
+                << "\nConclusion: " << conclusion << "\n";
+            // Failed. So flip sub and try again
+            subs[0][1] = conclusionTermEq[1];
+            subs[1][1] = conclusionTermEq[0];
+            substConclusionInReverseOrder = false;
+            continue;
+          }
+          // build next chain
+          std::vector<Node> copy2ofExpPremises(expansionPremises.begin(),
+                                               expansionPremises.end());
+          Node transConclusion2 = subs[1][0].eqNode(subs[1][1]);
+          if (!buildTransitivityChain(transConclusion2, copy2ofExpPremises))
+          {
+            Unreachable() << "Found sub " << transConclusion1
+                          << " but not other sub " << transConclusion2
+                          << ".\nDisequality: " << premises[offending]
+                          << "\nExpansion premises: " << expansionPremises
+                          << "\nConclusion: " << conclusion << "\n";
+          }
+          Trace("eqproof-conv")
+              << "EqProof::expandTransitivityForDisequalities: Built trans "
+                 "chains: "
+                 "for two subs among more than 2 premises:\n";
+          Trace("eqproof-conv")
+              << "EqProof::expandTransitivityForDisequalities: "
+              << transConclusion1 << " <- " << copy1ofExpPremises << "\n";
+          Trace("eqproof-conv")
+              << "EqProof::expandTransitivityForDisequalities: "
+              << transConclusion2 << " <- " << copy2ofExpPremises << "\n";
+          // do transitivity steps if need be to justify each substitution
+          if (copy1ofExpPremises.size() > 1
+              && !assumptions.count(transConclusion1))
+          {
+            p->addStep(
+                transConclusion1, PfRule::TRANS, copy1ofExpPremises, {}, true);
+          }
+          if (copy2ofExpPremises.size() > 1
+              && !assumptions.count(transConclusion2))
+          {
+            p->addStep(
+                transConclusion2, PfRule::TRANS, copy2ofExpPremises, {}, true);
+          }
+        }
+      }
+    }
+    Trace("eqproof-conv")
+        << "EqProof::expandTransitivityForDisequalities: Built substutitions "
+        << subs[0] << " and " << subs[1] << " to map " << premiseTermEq
+        << " -> " << conclusionTermEq << "\n";
+    Assert(subs[0][1] == conclusion[0][0] || subs[0][1] == conclusion[0][1])
+        << "EqProof::expandTransitivityForDisequalities: First substitution "
+        << subs[0] << " doest not map to conclusion " << conclusion << "\n";
+    Assert(subs[1][1] == conclusion[0][0] || subs[1][1] == conclusion[0][1])
+        << "EqProof::expandTransitivityForDisequalities: Second substitution "
+        << subs[1] << " doest not map to conclusion " << conclusion << "\n";
+    // In the premises for the original conclusion, the substitution of
+    // premiseTermEq (= t1 t2) into conclusionTermEq (= t3 t4) is stored
+    // reversed, i.e. as (= (= t3 t4) (= t1 t2)), since the transitivity with
+    // the disequality is built as as
+    //   (= (= t3 t4) (= t1 t2))                         (= (= t1 t2) false)
+    //  --------------------------------------------------------------------- TR
+    //                      (= (= t3 t4) false)
+    substPremises.push_back(subs[0][1].eqNode(subs[0][0]));
+    substPremises.push_back(subs[1][1].eqNode(subs[1][0]));
+  }
+  else
+  {
+    // In simple case the conclusion is always, modulo symmetry, false = true
+    Assert(conclusion[0].getKind() == kind::CONST_BOOLEAN
+           && conclusion[1].getKind() == kind::CONST_BOOLEAN);
+    // The expansion conclusion is the same as the equality term in the
+    // disequality, which is going to be justified by a transitivity step from
+    // the expansion premises
+    expansionConclusion = premises[offending][termPos];
+  }
+  // Unless we are in the double-substitution case, the proof has the shape
+  //
+  //                           ... ... ... ...         - expansionPremises
+  //                          ------------------ TRANS
+  //     (= (= (t t') false)    (= t'' t''')           - expansionConclusion
+  //  ---------------------------------------------- TRANS or PRED_TRANSFORM
+  //             conclusion
+  //
+  // although note that if it's a TRANS step, (= t'' t''') will be turned into a
+  // predicate equality and the premises are ordered.
+  //
+  // We build the transitivity step for the expansionConclusion here. It being
+  // non-null marks that we are not in the double-substitution case.
+  if (!expansionConclusion.isNull())
+  {
+    Trace("eqproof-conv")
+        << "EqProof::expandTransitivityForDisequalities: need to derive "
+        << expansionConclusion << " with premises " << expansionPremises
+        << "\n";
+    Assert(expansionPremises.size() > 1
+           || expansionConclusion == expansionPremises.back()
+           || (expansionConclusion[0] == expansionPremises.back()[1]
+               && expansionConclusion[1] == expansionPremises.back()[0]))
+        << "single expansion premise " << expansionPremises.back()
+        << " is not the same as expansionConclusion " << expansionConclusion
+        << " and not its symmetric\n";
+    // We track assumptions to avoid cyclic proofs, which can happen in EqProofs
+    // such as:
+    //
+    //              (= l1 "")     (= "" t)
+    //            ----------------------- EQP::TR
+    //  (= l1 "")           (= l1 t)                  (= (= "" t) false)
+    // ----------------------------------------------------------------- EQP::TR
+    //                        (= false true)
+    //
+    // which would lead to the cyclic expansion proof:
+    //
+    //       (= l1 "")             (= l1 "")   (= "" t)
+    //       --------- SYMM      ----------------------- TRANS
+    //       (= "" l1)                     (= l1 t)
+    //      ------------------------------------------ TRANS
+    //                       (= "" t)
+    if (expansionPremises.size() > 1 && !assumptions.count(expansionConclusion))
+    {
+      // create transitivity step to derive expected premise
+      buildTransitivityChain(expansionConclusion, expansionPremises);
+      Trace("eqproof-conv")
+          << "EqProof::expandTransitivityForDisequalities: add transitivity "
+             "step for "
+          << expansionConclusion << " with premises " << expansionPremises
+          << "\n";
+      // create expansion step
+      p->addStep(
+          expansionConclusion, PfRule::TRANS, expansionPremises, {}, true);
+    }
+  }
+  Trace("eqproof-conv")
+      << "EqProof::expandTransitivityForDisequalities: now derive conclusion "
+      << conclusion;
+  premises.clear();
+  premises.push_back(premises[offending]);
+  if (inSubstCase)
+  {
+    Trace("eqproof-conv") << (substConclusionInReverseOrder ? " [inverted]"
+                                                            : "")
+                          << " via subsitution from " << premises[offending]
+                          << " and (inverted subst) " << substPremises << "\n";
+    //  By this point, for premise disequality (= (= t1 t2) false), we have
+    //  potentially already built
+    //
+    //     (= t1 x1) ... (= xn t3)      (= t2 y1) ... (= ym t4)
+    //    ------------------------ TR  ------------------------ TR
+    //     (= t1 t3)                    (= t2 t4)
+    //
+    // to justify the substitutions t1->t3 and t2->t4 (where note that if t1=t3
+    // or t2=4, the step will actually be a REFL one). Not do
+    //
+    //  ----------- SYMM             ----------- SYMM
+    //   (= t3 t1)                    (= t4 t2)
+    //  ---------------------------------------- CONG
+    //   (= (= t3 t4) (= t1 t2))                         (= (= t1 t2) false)
+    //  --------------------------------------------------------------------- TR
+    //                   (= (= t3 t4) false)
+    //
+    // where note that the SYMM steps are implicitly added by CDProof.
+    Node congConclusion = nm->mkNode(
+        kind::EQUAL,
+        nm->mkNode(kind::EQUAL, substPremises[0][0], substPremises[1][0]),
+        premises[offending][0]);
+    p->addStep(congConclusion,
+               PfRule::CONG,
+               substPremises,
+               {nm->operatorOf(kind::EQUAL)},
+               true);
+    Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via "
+                             "congruence derived "
+                          << congConclusion << "\n";
+    // transitivity step between that and the original premise
+    premises.insert(premises.begin(), congConclusion);
+    Node transConclusion =
+        !substConclusionInReverseOrder
+            ? conclusion
+            : nm->mkNode(kind::EQUAL, congConclusion[0], conclusion[1]);
+    // check to avoid cyclic proofs
+    if (!assumptions.count(transConclusion))
+    {
+      p->addStep(transConclusion, PfRule::TRANS, premises, {}, true);
+      Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
+                               "via transitivity derived "
+                            << transConclusion << "\n";
+    }
+    // if order is reversed, finish the proof of conclusion with
+    //           (= (= t3 t4) false)
+    //          --------------------- MACRO_SR_PRED_TRANSFORM
+    //           (= (= t4 t3) false)
+    if (substConclusionInReverseOrder)
+    {
+      p->addStep(conclusion,
+                 PfRule::MACRO_SR_PRED_TRANSFORM,
+                 {transConclusion},
+                 {conclusion},
+                 true);
+      Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: "
+                               "via macro transform derived "
+                            << conclusion << "\n";
+    }
+  }
+  else
+  {
+    // create TRUE_INTRO step for expansionConclusion and add it to the premises
+    Trace("eqproof-conv")
+        << " via transitivity.\nEqProof::expandTransitivityForDisequalities: "
+           "adding "
+        << PfRule::TRUE_INTRO << " step for " << expansionConclusion[0] << "\n";
+    Node newExpansionConclusion =
+        expansionConclusion.eqNode(nm->mkConst<bool>(true));
+    p->addStep(
+        newExpansionConclusion, PfRule::TRUE_INTRO, {expansionConclusion}, {});
+    premises.push_back(newExpansionConclusion);
+    Trace("eqproof-conv") << PfRule::TRANS << " from " << premises << "\n";
+    buildTransitivityChain(conclusion, premises);
+    // create final transitivity step
+    p->addStep(conclusion, PfRule::TRANS, premises, {}, true);
+  }
+  return true;
 }
 
 bool EqProof::buildTransitivityChain(Node conclusion,
                                      std::vector<Node>& premises) const
 {
+  Trace("eqproof-conv") << push
+                        << "EqProof::buildTransitivityChain: Build chain for "
+                        << conclusion << " with premises " << premises << "\n";
+  for (unsigned i = 0, size = premises.size(); i < size; ++i)
+  {
+    bool occurs = false, correctlyOrdered = false;
+    if (conclusion[0] == premises[i][0])
+    {
+      occurs = correctlyOrdered = true;
+    }
+    else if (conclusion[0] == premises[i][1])
+    {
+      occurs = true;
+    }
+    if (occurs)
+    {
+      Trace("eqproof-conv")
+          << "EqProof::buildTransitivityChain: found " << conclusion[0] << " in"
+          << (correctlyOrdered ? "" : " non-") << " ordered premise "
+          << premises[i] << "\n";
+      if (conclusion[1] == premises[i][correctlyOrdered ? 1 : 0])
+      {
+        Trace("eqproof-conv")
+            << "EqProof::buildTransitivityChain: found " << conclusion[1]
+            << " in same premise. Closed chain.\n"
+            << pop;
+        premises.clear();
+        premises.push_back(conclusion);
+        return true;
+      }
+      // Build chain with remaining equalities
+      std::vector<Node> recursivePremises;
+      for (unsigned j = 0; j < size; ++j)
+      {
+        if (j != i)
+        {
+          recursivePremises.push_back(premises[j]);
+        }
+      }
+      Node newTarget =
+          premises[i][correctlyOrdered ? 1 : 0].eqNode(conclusion[1]);
+      Trace("eqproof-conv")
+          << "EqProof::buildTransitivityChain: search recursively for "
+          << newTarget << "\n";
+      if (buildTransitivityChain(newTarget, recursivePremises))
+      {
+        Trace("eqproof-conv")
+            << "EqProof::buildTransitivityChain: closed chain with "
+            << 1 + recursivePremises.size() << " of the original "
+            << premises.size() << " premises\n"
+            << pop;
+        premises.clear();
+        premises.insert(premises.begin(),
+                        correctlyOrdered
+                            ? premises[i]
+                            : premises[i][1].eqNode(premises[i][0]));
+        premises.insert(
+            premises.end(), recursivePremises.begin(), recursivePremises.end());
+        return true;
+      }
+    }
+  }
+  Trace("eqproof-conv")
+      << "EqProof::buildTransitivityChain: Could not build chain for"
+      << conclusion << " with premises " << premises << "\n";
+  Trace("eqproof-conv") << pop;
   return false;
 }
 
@@ -112,16 +616,673 @@ void EqProof::reduceNestedCongruence(
     std::unordered_set<Node, NodeHashFunction>& assumptions,
     bool isNary) const
 {
+  Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i
+                        << "-th arg\n";
+  if (d_id == MERGED_THROUGH_CONGRUENCE)
+  {
+    Assert(d_children.size() == 2);
+    Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
+                             "congruence step. Reduce second child\n"
+                          << push;
+    transitivityMatrix[i].push_back(
+        d_children[1]->addToProof(p, visited, assumptions));
+    Trace("eqproof-conv")
+        << pop << "EqProof::reduceNestedCongruence: child conclusion "
+        << transitivityMatrix[i].back() << "\n";
+    // if i == 0, first child must be REFL step, standing for (= f f), which can
+    // be ignored in a first-order calculus
+    Assert(i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY);
+    // recurse
+    if (i > 0)
+    {
+      Trace("eqproof-conv")
+          << "EqProof::reduceNestedCongruence: Reduce first child\n"
+          << push;
+      d_children[0]->reduceNestedCongruence(i - 1,
+                                            conclusion,
+                                            transitivityMatrix,
+                                            p,
+                                            visited,
+                                            assumptions,
+                                            isNary);
+      Trace("eqproof-conv") << pop;
+    }
+    return;
+  }
+  Assert(d_id == MERGED_THROUGH_TRANS);
+  Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
+                           "transitivity step.\n";
+  Assert(d_node.isNull()
+         || d_node[0].getNumChildren() == d_node[1].getNumChildren() || isNary)
+      << "Non-null (internal cong) transitivity conclusion of different arity "
+         "but not marked by isNary flag\n";
+  // If handling n-ary kinds and got a transitivity conclusion, we process it
+  // with addToProof, store the result into row i, and stop. This marks an
+  // "adjustment" of the arity, with empty rows 0..i-1 in the matrix determining
+  // the adjustment in addToProof processing the congruence of the original
+  // conclusion. See details there.
+  if (isNary && !d_node.isNull())
+  {
+    Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: n-ary case, "
+                             "break recursion and indepedently process "
+                          << d_node << "\n"
+                          << push;
+    transitivityMatrix[i].push_back(addToProof(p, visited, assumptions));
+    Trace("eqproof-conv") << pop
+                          << "EqProof::reduceNestedCongruence: Got conclusion "
+                          << transitivityMatrix[i].back()
+                          << " from n-ary transitivity processing\n";
+    return;
+  }
+  // Regular recursive processing of each transitivity premise
+  for (unsigned j = 0, sizeTrans = d_children.size(); j < sizeTrans; ++j)
+  {
+    if (d_children[j]->d_id == MERGED_THROUGH_CONGRUENCE)
+    {
+      Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Reduce " << j
+                            << "-th transitivity congruence child\n"
+                            << push;
+      d_children[j]->reduceNestedCongruence(
+          i, conclusion, transitivityMatrix, p, visited, assumptions, isNary);
+      Trace("eqproof-conv") << pop;
+    }
+    else
+    {
+      Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: Add " << j
+                            << "-th transitivity child to proof\n"
+                            << push;
+      transitivityMatrix[i].push_back(
+          d_children[j]->addToProof(p, visited, assumptions));
+      Trace("eqproof-conv") << pop;
+    }
+  }
 }
 
-Node EqProof::addToProof(CDProof* p) const { return Node::null(); }
+Node EqProof::addToProof(CDProof* p) const
+{
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  std::unordered_set<Node, NodeHashFunction> assumptions;
+  Node conclusion = addToProof(p, cache, assumptions);
+  Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion
+                        << "\n";
+  Trace("eqproof-conv") << "EqProof::addToProof: tracked assumptions: "
+                        << assumptions << "\n";
+  // If conclusion t1 = tn is, modulo symmetry, of the form (= t true/false), in
+  // which t is not true/false, it must be turned into t or (not t) with
+  // TRUE/FALSE_ELIM.
+  Node newConclusion = conclusion;
+  Assert(conclusion.getKind() == kind::EQUAL);
+  if ((conclusion[0].getKind() == kind::CONST_BOOLEAN)
+      != (conclusion[1].getKind() == kind::CONST_BOOLEAN))
+  {
+    Trace("eqproof-conv")
+        << "EqProof::addToProof: process root for TRUE/FALSE_ELIM\n";
+    // Index of constant in equality
+    unsigned constIndex =
+        conclusion[0].getKind() == kind::CONST_BOOLEAN ? 0 : 1;
+    // The premise for the elimination rule must have the constant as the second
+    // argument of the equality. If that's not the case, build it as such,
+    // relying on an implicit SYMM step to be added to the proof when justifying
+    // t / (not t).
+    Node elimPremise =
+        constIndex == 1 ? conclusion : conclusion[1].eqNode(conclusion[0]);
+    // Determine whether TRUE_ELIM or FALSE_ELIM, depending on the constant
+    // value. The new conclusion, whether t or (not t), is also determined
+    // accordingly.
+    PfRule elimRule;
+    if (conclusion[constIndex].getConst<bool>())
+    {
+      elimRule = PfRule::TRUE_ELIM;
+      newConclusion = conclusion[1 - constIndex];
+    }
+    else
+    {
+      elimRule = PfRule::FALSE_ELIM;
+      newConclusion = conclusion[1 - constIndex].notNode();
+    }
+    // We also check if the final conclusion t / (not t) has already been
+    // justified, so that we can avoid a cyclic proof, which can be due to
+    // either t / (not t) being assumption in the original EqProof or it having
+    // a non-assumption proof step in the proof of (= t true/false).
+    if (!assumptions.count(newConclusion) && !p->hasStep(newConclusion))
+    {
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: conclude " << newConclusion << " via "
+          << elimRule << " step for " << elimPremise << "\n";
+      p->addStep(newConclusion, elimRule, {elimPremise}, {});
+    }
+  }
+  return newConclusion;
+}
 
 Node EqProof::addToProof(
     CDProof* p,
     std::unordered_map<Node, Node, NodeHashFunction>& visited,
     std::unordered_set<Node, NodeHashFunction>& assumptions) const
 {
-  return Node::null();
+  std::unordered_map<Node, Node, NodeHashFunction>::const_iterator it =
+      visited.find(d_node);
+  if (it != visited.end())
+  {
+    Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node
+                          << ", returning " << it->second << "\n";
+    return it->second;
+  }
+  Trace("eqproof-conv") << "EqProof::addToProof: adding step for "
+                        << static_cast<MergeReasonType>(d_id)
+                        << " with conclusion " << d_node << "\n";
+  // Assumption
+  if (d_id == MERGED_THROUGH_EQUALITY)
+  {
+    // Check that no (= true/false true/false) assumptions
+    if (Configuration::isDebugBuild() && d_node.getKind() == kind::EQUAL)
+    {
+      for (unsigned i = 0; i < 2; ++i)
+      {
+        Assert(d_node[i].getKind() != kind::CONST_BOOLEAN
+               || d_node[1 - i].getKind() != kind::CONST_BOOLEAN)
+            << "EqProof::addToProof: fully boolean constant assumption "
+            << d_node << " is disallowed\n";
+      }
+    }
+    // If conclusion is (= t true/false), we add a proof step
+    //          t
+    //  ---------------- TRUE/FALSE_INTRO
+    //  (= t true/false)
+    // according to the value of the Boolean constant
+    if (d_node.getKind() == kind::EQUAL
+        && ((d_node[0].getKind() == kind::CONST_BOOLEAN)
+            != (d_node[1].getKind() == kind::CONST_BOOLEAN)))
+    {
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: add an intro step for " << d_node << "\n";
+      // Index of constant in equality
+      unsigned constIndex = d_node[0].getKind() == kind::CONST_BOOLEAN ? 0 : 1;
+      // The premise for the intro rule is either t or (not t), according to the
+      // Boolean constant.
+      Node introPremise;
+      PfRule introRule;
+      if (d_node[constIndex].getConst<bool>())
+      {
+        introRule = PfRule::TRUE_INTRO;
+        introPremise = d_node[1 - constIndex];
+        // Track the new assumption. If it's an equality, also its symmetric
+        assumptions.insert(introPremise);
+        if (introPremise.getKind() == kind::EQUAL)
+        {
+          assumptions.insert(introPremise[1].eqNode(introPremise[0]));
+        }
+      }
+      else
+      {
+        introRule = PfRule::FALSE_INTRO;
+        introPremise = d_node[1 - constIndex].notNode();
+        // Track the new assumption. If it's a disequality, also its symmetric
+        assumptions.insert(introPremise);
+        if (introPremise[0].getKind() == kind::EQUAL)
+        {
+          assumptions.insert(
+              introPremise[0][1].eqNode(introPremise[0][0]).notNode());
+        }
+      }
+      // The original assumption can be e.g. (= false (= t1 t2)) in which case
+      // the necessary proof to be built is
+      //     (not (= t1 t2))
+      //  -------------------- FALSE_INTRO
+      //  (= (= t1 t2) false)
+      //  -------------------- SYMM
+      //  (= false (= t1 t2))
+      //
+      // with the SYMM step happening automatically whenever the assumption is
+      // used in the proof p
+      Node introConclusion =
+          constIndex == 1 ? d_node : d_node[1].eqNode(d_node[0]);
+      p->addStep(introConclusion, introRule, {introPremise}, {});
+    }
+    else
+    {
+      p->addStep(d_node, PfRule::ASSUME, {}, {d_node});
+    }
+    // If non-equality predicate, turn into one via TRUE/FALSE intro
+    Node conclusion = d_node;
+    if (d_node.getKind() != kind::EQUAL)
+    {
+      // Track original assumption
+      assumptions.insert(d_node);
+      PfRule intro;
+      if (d_node.getKind() == kind::NOT)
+      {
+        intro = PfRule::FALSE_INTRO;
+        conclusion =
+            d_node[0].eqNode(NodeManager::currentNM()->mkConst<bool>(false));
+      }
+      else
+      {
+        intro = PfRule::TRUE_INTRO;
+        conclusion =
+            d_node.eqNode(NodeManager::currentNM()->mkConst<bool>(true));
+      }
+      Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro
+                            << " step for " << d_node << "\n";
+      p->addStep(conclusion, intro, {d_node}, {});
+    }
+    // Keep track of assumptions to avoid cyclic proofs. Both the assumption and
+    // its symmetric are added
+    assumptions.insert(conclusion);
+    assumptions.insert(conclusion[1].eqNode(conclusion[0]));
+    Trace("eqproof-conv") << "EqProof::addToProof: tracking assumptions "
+                          << conclusion << ", (= " << conclusion[1] << " "
+                          << conclusion[0] << ")\n";
+    visited[d_node] = conclusion;
+    return conclusion;
+  }
+  // Refl and laborious congruence steps for (= (f t1 ... tn) (f t1 ... tn)),
+  // which can be safely turned into reflexivity steps. These laborious
+  // congruence steps are currently generated in the equality engine because of
+  // the suboptimal handling of n-ary operators.
+  if (d_id == MERGED_THROUGH_REFLEXIVITY
+      || (d_node.getKind() == kind::EQUAL && d_node[0] == d_node[1]))
+  {
+    Node conclusion =
+        d_node.getKind() == kind::EQUAL ? d_node : d_node.eqNode(d_node);
+    p->addStep(conclusion, PfRule::REFL, {}, {conclusion[0]});
+    visited[d_node] = conclusion;
+    return conclusion;
+  }
+  // Equalities due to theory reasoning
+  if (d_id == MERGED_THROUGH_CONSTANTS)
+  {
+    // Currently only supports case of negative merged throgh constants
+    Assert(!d_node.isNull() && d_node.getKind() == kind::EQUAL
+           && d_node[0].getKind() == kind::EQUAL
+           && d_node[1].getKind() == kind::CONST_BOOLEAN
+           && !d_node[1].getConst<bool>())
+        << ". Conclusion " << d_node << " from "
+        << static_cast<MergeReasonType>(d_id)
+        << " was expected to be (= (= t1 t2) false)\n";
+    Assert(!assumptions.count(d_node))
+        << "Conclusion " << d_node << " from "
+        << static_cast<MergeReasonType>(d_id) << " is an assumption\n";
+    // The step has the form
+    //  [(= t1 c1)]  [(= t2 c2)]
+    //  ------------------------
+    //    (= (= t1 t2) false)
+    // where premises equating t1/t2 to constants are present when they are not
+    // already constants. Note that the premises may be in any order, e.g. with
+    // the equality for the second term being justified in the first premise.
+    // Moreover, they may be of the form (= c t).
+    //
+    // First recursively process premises, if any
+    std::vector<Node> premises;
+    for (unsigned i = 0; i < d_children.size(); ++i)
+    {
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: recurse on child " << i << "\n"
+          << push;
+      premises.push_back(d_children[i]->addToProof(p, visited, assumptions));
+      Trace("eqproof-conv") << pop;
+    }
+    // A step
+    //  [(= t1 c1)]  [(= t2 c2)]
+    //  ------------------------ MACRO_SR_PRED_INTRO
+    //    (= (= t1 t2) false)
+    // is gonna be built, with the premises is the correct order.
+    std::vector<Node> children;
+    for (unsigned i = 0; i < 2; ++i)
+    {
+      Node term = d_node[0][i];
+      // term already is a constant, no need to add a premise to it
+      if (term.isConst())
+      {
+        continue;
+      }
+      // Build the equality (= t c) as a premise, finding the respective c is
+      // the original premises
+      Node constant;
+      for (const Node& premise : premises)
+      {
+        Assert(premise.getKind() == kind::EQUAL);
+        if (premise[0] == term)
+        {
+          Assert(premise[1].isConst());
+          constant = premise[1];
+        }
+        else if (premise[1] == term)
+        {
+          Assert(premise[0].isConst());
+          constant = premise[0];
+        }
+      }
+      children.push_back(term.eqNode(constant));
+    }
+    Trace("eqproof-conv") << "EqProof::addToProof: adding "
+                          << PfRule::MACRO_SR_PRED_INTRO << " step from "
+                          << children << "\n";
+    p->addStep(d_node, PfRule::MACRO_SR_PRED_INTRO, children, {d_node});
+    visited[d_node] = d_node;
+    return d_node;
+  }
+  // Transtivity and disequality reasoning steps
+  if (d_id == MERGED_THROUGH_TRANS)
+  {
+    Assert(d_node.getKind() == kind::EQUAL
+           || (d_node.getKind() == kind::NOT
+               && d_node[0].getKind() == kind::EQUAL))
+        << "EqProof::addToProof: transitivity step conclusion " << d_node
+        << " is not equality or negated equality\n";
+    // If conclusion is (not (= t1 t2)) change it to (= (= t1 t2) false), which
+    // is the correct conclusion of the equality reasoning step. A FALSE_ELIM
+    // step to revert this is only necessary when this is the root. That step is
+    // done in the non-recursive caller of this function.
+    Node conclusion =
+        d_node.getKind() != kind::NOT
+            ? d_node
+            : d_node[0].eqNode(NodeManager::currentNM()->mkConst<bool>(false));
+    // If the conclusion is an assumption, its derivation was spurious, so it
+    // can be discarded. Moreover, reconstructing the step may lead to cyclic
+    // proofs, so we *must* cut here.
+    if (assumptions.count(conclusion))
+    {
+      visited[d_node] = conclusion;
+      return conclusion;
+    }
+    // Process premises recursively
+    std::vector<Node> children;
+    for (unsigned i = 0, size = d_children.size(); i < size; ++i)
+    {
+      // If one of the steps is a "fake congruence" one, marked by a null
+      // conclusion, it must deleted. Its premises are moved down to premises of
+      // the transitivity step.
+      EqProof* childProof = d_children[i].get();
+      if (childProof->d_id == MERGED_THROUGH_CONGRUENCE
+          && childProof->d_node.isNull())
+      {
+        CVC4_UNUSED bool addedChild = false;
+        Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i
+                              << " is fake cong step. Fold it.\n";
+        Assert(childProof->d_children.size() == 2);
+        Trace("eqproof-conv") << push;
+        for (unsigned j = 0, sizeJ = childProof->d_children.size(); j < sizeJ;
+             ++j)
+        {
+          Trace("eqproof-conv")
+              << "EqProof::addToProof: recurse on child " << j << "\n"
+              << push;
+          Node child =
+              childProof->d_children[j]->addToProof(p, visited, assumptions);
+          Trace("eqproof-conv") << pop;
+        }
+        Trace("eqproof-conv") << pop;
+        Assert(addedChild);
+        continue;
+      }
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: recurse on child " << i << "\n"
+          << push;
+      children.push_back(childProof->addToProof(p, visited, assumptions));
+      Trace("eqproof-conv") << pop;
+    }
+    // Eliminate spurious premises. Reasoning below assumes no refl steps.
+    cleanReflPremises(children);
+    // If any premise is of the form (= (t1 t2) false), then the transitivity
+    // step may be coarse-grained and needs to be expanded. If the expansion
+    // happens it also finalizes the proof of conclusion.
+    if (!expandTransitivityForDisequalities(
+            conclusion, children, p, assumptions))
+    {
+      Assert(!children.empty());
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: build chain for transitivity premises"
+          << children << " to conclude " << conclusion << "\n";
+      // Build ordered transitivity chain from children to derive the conclusion
+      buildTransitivityChain(conclusion, children);
+      Assert(children.size() > 1
+             || (!children.empty()
+                 && (children[0] == conclusion
+                     || children[0][1].eqNode(children[0][0]) == conclusion)));
+      // Only add transitivity step if there is more than one premise in the
+      // chain. Otherwise the premise will be the conclusion itself and it'll
+      // already have had a step added to it when the premises were recursively
+      // processed.
+      if (children.size() > 1)
+      {
+        p->addStep(conclusion, PfRule::TRANS, children, {}, true);
+      }
+    }
+    Assert(p->hasStep(conclusion));
+    visited[d_node] = conclusion;
+    return conclusion;
+  }
+  Assert(d_id == MERGED_THROUGH_CONGRUENCE);
+  // The processing below is mainly dedicated to flattening congruence steps
+  // (since EqProof assumes currying) and to prossibly reconstructing the
+  // conclusion in case it involves n-ary steps.
+  Assert(d_node.getKind() == kind::EQUAL)
+      << "EqProof::addToProof: conclusion " << d_node << " is not equality\n";
+  // The given conclusion is taken as ground truth. If the premises do not
+  // align, for example with (= (f t1) (f t2)) but a premise being (= t2 t1), we
+  // use (= t1 t2) as a premise and rely on a symmetry step to justify it.
+  unsigned arity = d_node[0].getNumChildren();
+  Kind k = d_node[0].getKind();
+  bool isNary = ExprManager::isNAryKind(k);
+
+  // N-ary operators are fun. The following proof is a valid EqProof
+  //
+  //   (= (f t1 t2 t3) (f t6 t5)) (= (f t6 t5) (f t5 t6))
+  //   -------------------------------------------------- TRANS
+  //             (= (f t1 t2 t3) (f t5 t6))                      (= t4 t7)
+  //          ------------------------------------------------------------ CONG
+  //          (= (f t1 t2 t3 t4) (f t5 t6 t7))
+  //
+  // We modify the above proof to conclude
+  //
+  //   (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7))
+  //
+  // which is a valid congruence conclusion (applications of f with the same
+  // arity). For the processing below to be//  performed correctly we update
+  // arity to be maximal one among the two applications (4 in the above
+  // example).
+  if (d_node[0].getNumChildren() != d_node[1].getNumChildren())
+  {
+    Assert(isNary);
+    arity =
+        d_node[1].getNumChildren() < arity ? arity : d_node[1].getNumChildren();
+    Trace("eqproof-conv")
+        << "EqProof::addToProof: Mismatching arities in cong conclusion "
+        << d_node << ". Use tentative arity " << arity << "\n";
+  }
+  // For a congruence proof of (= (f a0 ... an-1) (f b0 ... bn-1)), build a
+  // transitivity matrix where each row contains a transitivity chain justifying
+  // (= ai bi)
+  std::vector<std::vector<Node>> transitivityChildren;
+  for (unsigned i = 0; i < arity; ++i)
+  {
+    transitivityChildren.push_back(std::vector<Node>());
+  }
+  reduceNestedCongruence(
+      arity - 1, d_node, transitivityChildren, p, visited, assumptions, isNary);
+  // Congruences over n-ary operators may require changing the conclusion (as in
+  // the above example). This is handled in a general manner below according to
+  // whether the transitivity matrix computed by reduceNestedCongruence contains
+  // empty rows
+  Node conclusion = d_node;
+  NodeManager* nm = NodeManager::currentNM();
+  if (isNary)
+  {
+    unsigned emptyRows = 0;
+    for (unsigned i = 0; i < arity; ++i)
+    {
+      if (transitivityChildren[i].empty())
+      {
+        emptyRows++;
+      }
+    }
+    // Given two n-ary applications f1:(f a0 ... an-1), f2:(f b0 ... bm-1), of
+    // arities n and m, arity = max(n,m), the number emptyRows establishes the
+    // sizes of the prefixes of f1 of f2 that have been equated via a
+    // transitivity step. The prefixes necessarily have different sizes. The
+    // suffixes have the same sizes. The new conclusion will be of the form
+    //     (= (f (f a0 ... ak1) ... an-1) (f (f b0 ... bk2) ... bm-1))
+    // where
+    //  k1 = emptyRows + 1 - (arity - n)
+    //  k2 = emptyRows + 1 - (arity - m)
+    //  k1 != k2
+    //  n - k1 == m - k2
+    // Note that by construction the equality between the first emptyRows + 1
+    // arguments of each application is justified by the transitivity step in
+    // the row emptyRows +1 in the matrix.
+    if (emptyRows > 0)
+    {
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: Found " << emptyRows
+          << " empty rows. Rebuild conclusion " << d_node << "\n";
+      // New transitivity matrix is as before except that the empty rows in the
+      // beginning are eliminated, as the new arity is the maximal arity among
+      // the applications minus the number of empty rows.
+      std::vector<std::vector<Node>> newTransitivityChildren{
+          transitivityChildren.begin() + emptyRows, transitivityChildren.end()};
+      transitivityChildren.clear();
+      transitivityChildren.insert(transitivityChildren.begin(),
+                                  newTransitivityChildren.begin(),
+                                  newTransitivityChildren.end());
+      unsigned arityPrefix1 =
+          emptyRows + 1 - (arity - d_node[0].getNumChildren());
+      Assert(arityPrefix1 < d_node[0].getNumChildren())
+          << "arityPrefix1 " << arityPrefix1 << " not smaller than "
+          << d_node[0] << "'s arity " << d_node[0].getNumChildren() << "\n";
+      unsigned arityPrefix2 =
+          emptyRows + 1 - (arity - d_node[1].getNumChildren());
+      Assert(arityPrefix2 < d_node[1].getNumChildren())
+          << "arityPrefix2 " << arityPrefix2 << " not smaller than "
+          << d_node[1] << "'s arity " << d_node[1].getNumChildren() << "\n";
+      Trace("eqproof-conv") << "EqProof::addToProof: New internal "
+                               "applications with arities "
+                            << arityPrefix1 << ", " << arityPrefix2 << ":\n";
+      std::vector<Node> childrenPrefix1{d_node[0].begin(),
+                                        d_node[0].begin() + arityPrefix1};
+      std::vector<Node> childrenPrefix2{d_node[1].begin(),
+                                        d_node[1].begin() + arityPrefix2};
+      Node newFirstChild1 = nm->mkNode(k, childrenPrefix1);
+      Node newFirstChild2 = nm->mkNode(k, childrenPrefix2);
+      Trace("eqproof-conv")
+          << "EqProof::addToProof:\t " << newFirstChild1 << "\n";
+      Trace("eqproof-conv")
+          << "EqProof::addToProof:\t " << newFirstChild2 << "\n";
+      std::vector<Node> newChildren1{newFirstChild1};
+      newChildren1.insert(newChildren1.end(),
+                          d_node[0].begin() + arityPrefix1,
+                          d_node[0].end());
+      std::vector<Node> newChildren2{newFirstChild2};
+      newChildren2.insert(newChildren2.end(),
+                          d_node[1].begin() + arityPrefix2,
+                          d_node[1].end());
+      conclusion = nm->mkNode(kind::EQUAL,
+                              nm->mkNode(k, newChildren1),
+                              nm->mkNode(k, newChildren2));
+      // update arity
+      Assert((arity - emptyRows) == conclusion[0].getNumChildren());
+      arity = arity - emptyRows;
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: New conclusion " << conclusion << "\n";
+    }
+  }
+  if (Trace.isOn("eqproof-conv"))
+  {
+    Trace("eqproof-conv")
+        << "EqProof::addToProof: premises from reduced cong of " << conclusion
+        << ":\n";
+    for (unsigned i = 0; i < arity; ++i)
+    {
+      Trace("eqproof-conv") << "EqProof::addToProof:\t" << i
+                            << "-th arg: " << transitivityChildren[i] << "\n";
+    }
+  }
+  // Proccess transitivity matrix to (possibly) generate transitivity steps for
+  // congruence premises (= ai bi)
+  std::vector<Node> children(arity);
+  for (unsigned i = 0; i < arity; ++i)
+  {
+    Node transConclusion = conclusion[0][i].eqNode(conclusion[1][i]);
+    children[i] = transConclusion;
+    Assert(!transitivityChildren[i].empty())
+        << "EqProof::addToProof: did not add any justification for " << i
+        << "-th arg of congruence " << conclusion << "\n";
+    // If the transitivity conclusion is a reflexivity step, just add it. Note
+    // that this can happen with with transitivityChildren containing several
+    // equalities in the case of (= ai bi) being the same n-ary application that
+    // was justified by a congruence step, which can happen in the current
+    // equality engine
+    if (transConclusion[0] == transConclusion[1])
+    {
+      p->addStep(transConclusion, PfRule::REFL, {}, {transConclusion[0]});
+      continue;
+    }
+    // Remove spurious refl steps from the premises for (= ai bi)
+    cleanReflPremises(transitivityChildren[i]);
+    Assert(transitivityChildren[i].size() > 1 || transitivityChildren[i].empty()
+           || CDProof::isSame(transitivityChildren[i][0], transConclusion))
+        << "EqProof::addToProof: premises " << transitivityChildren[i] << "for "
+        << i << "-th cong premise " << transConclusion << " don't justify it\n";
+    unsigned sizeTrans = transitivityChildren[i].size();
+    // If no transitivity premise left or if (= ai bi) is an assumption (which
+    // might lead to a cycle with a transtivity step), nothing else to do.
+    if (sizeTrans == 0 || assumptions.count(transConclusion) > 0)
+    {
+      continue;
+    }
+    // If the transitivity conclusion, or its symmetric, occurs in the
+    // transitivity premises, nothing to do, as it is already justified and
+    // doing so again would lead to a cycle.
+    bool occurs = false;
+    for (unsigned j = 0; j < sizeTrans && !occurs; ++j)
+    {
+      if (CDProof::isSame(transitivityChildren[i][j], transConclusion))
+      {
+        occurs = true;
+      }
+    }
+    if (!occurs)
+    {
+      // Build transitivity step
+      buildTransitivityChain(transConclusion, transitivityChildren[i]);
+      Trace("eqproof-conv")
+          << "EqProof::addToProof: adding trans step for cong premise "
+          << transConclusion << " with children " << transitivityChildren[i]
+          << "\n";
+      p->addStep(
+          transConclusion, PfRule::TRANS, transitivityChildren[i], {}, true);
+    }
+  }
+  // Get node of the function operator over which congruence is being applied.
+  std::vector<Node> args;
+  if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
+  {
+    args.push_back(conclusion[0].getOperator());
+  }
+  else
+  {
+    args.push_back(nm->operatorOf(k));
+  }
+  // Add congruence step
+  Trace("eqproof-conv") << "EqProof::addToProof: build cong step of "
+                        << conclusion << " with op " << args[0]
+                        << " and children " << children << "\n";
+  p->addStep(conclusion, PfRule::CONG, children, args, true);
+  // If the conclusion of the congruence step changed due to the n-ary handling,
+  // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is
+  // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via
+  // rewriting
+  if (conclusion != d_node)
+  {
+    Trace("eqproof-conv") << "EqProof::addToProof: add "
+                          << PfRule::MACRO_SR_PRED_TRANSFORM
+                          << " step to flatten rebuilt conclusion "
+                          << conclusion << "into " << d_node << "\n";
+    p->addStep(
+        d_node, PfRule::MACRO_SR_PRED_TRANSFORM, {conclusion}, {d_node}, true);
+  }
+  visited[d_node] = d_node;
+  return d_node;
 }
 
 }  // namespace eq
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
index c396da313..ac440dc84 100644
--- a/src/theory/uf/eq_proof.h
+++ b/src/theory/uf/eq_proof.h
@@ -116,7 +116,7 @@ class EqProof
    * Currently the equality engine can represent disequality reasoning in a
    * rather coarse-grained manner with EqProof. This is always the case when the
    * transitivity step contains a disequality, (= (= t t') false) or its
-   * symmetric.
+   * symmetric, as a premise.
    *
    * There are two cases. In the simplest one the general shape of the EqProof
    * is
@@ -180,6 +180,9 @@ class EqProof
    * EqProof. These are necessary to avoid cyclic proofs, which could be
    * generated by creating transitivity steps for assumptions (which depend on
    * themselves).
+   * @return True if the EqProof transitivity step is in either of the above
+   * cases, symbolizing that the ProofNode justifying the conclusion has already
+   * beenproduced.
    */
   bool expandTransitivityForDisequalities(
       Node conclusion,