Function vivify_clause 

pub fn vivify_clause(
    num_vars: usize,
    db: &[Vec<Lit>],
    c: &[Lit],
) -> Option<Vec<Lit>>

Vivify a clause: drop every literal whose removal leaves a clause still RUP-implied by db. Returns the strengthened (shorter) clause, or None if nothing could be removed. The result is a sub-clause logically equivalent in context, so it is verdict-invariant.