+ // The lhs and rhs clauses in a binary resolution step, respectively. Since
+ // children correspond to the premises in the resolution chain, the first
+ // lhs clause is the first premise, the first rhs clause is the second
+ // premise. Each subsequent lhs clause will be the result of the previous
+ // binary resolution step in the chain, while each subsequent rhs clause
+ // will be respectively the second, third etc premises.
+ std::vector<Node> lhsClause, rhsClause;
+ // The pivots to be eliminated to the lhs clause and rhs clause in a binary
+ // resolution step, respectively
+ Node lhsElim, rhsElim;
+ // Get lhsClause of first resolution.
+ //
+ // Since a Node cannot hold an OR with a single child we need to
+ // disambiguate singleton clauses that are OR nodes from non-singleton
+ // clauses (i.e. unit clauses in the SAT solver).
+ //
+ // If the child is not an OR, it is a singleton clause and we take the
+ // child itself as the clause. Otherwise the child can only be a singleton
+ // clause if the child itself is used as a resolution literal, i.e. if the
+ // first child equal to the first pivot (which is args[1] or
+ // args[1].notNote() depending on the polarity).
+ if (children[0].getKind() != kind::OR
+ || (args[0] == trueNode && children[0] == args[1])
+ || (args[0] == falseNode && children[0] == args[1].notNode()))
+ {
+ lhsClause.push_back(children[0]);
+ }
+ else