Function log_progress 

pub fn log_progress(
    level: Level,
    done: usize,
    prev: usize,
    total: usize,
    step: usize,
    depth: usize,
)

One progress line per step boundary that prev → done crosses (increments may exceed 1, e.g. equivariant eliminations consume τ-pairs). depth indents by two spaces per level.