pub fn solve(clauses: &[HornClause], num_vars: usize) -> HornOutcomeExpand description
Solve a Horn system over 0..num_vars by forward chaining. Returns the least model, or — if a
goal clause is forced — a certified derivation. Linear in the total clause size.