Function query_with_cut 

pub fn query_with_cut(
    aig: &Aig,
    a: AigLit,
    b: AigLit,
    cut: &[u32],
    earlier: &[(AigLit, AigLit)],
) -> Query

The Tseitin clauses of the cone of a and b in node order, a node of cut (sorted) left free, then the two clauses of each earlier lemma with a literal in that cone, in lemma order (its other node, when outside the cone, a free variable of its own: lemmas joined through a representative the cone does not reach still join), then a ≠ b as (a ∨ b) ∧ (¬a ∨ ¬b).