Function ground_sorted 

pub fn ground_sorted(
    e: &ProofExpr,
    sorts: &HashMap<String, Vec<ProofTerm>>,
    fallback: &[ProofTerm],
) -> ProofExpr

SORT-AWARE grounding: a guarded quantifier expands only over its sort’s domain (∀x(Trip(x)→…) over the trips), falling back to fallback (the full universe) for an unsorted quantifier. Sound for a domain-closed problem and dramatically smaller than universe-grounding — the optimization the larger puzzles need.