Function ground_problem_sorted 

pub fn ground_problem_sorted(
    premises: &[ProofExpr],
    goal: &ProofExpr,
) -> (Vec<ProofExpr>, ProofExpr)

ground_problem but sort-aware (each quantifier grounds over its guard sort). The default entry point for finite-domain solving.