Function detect_conflict 

pub fn detect_conflict(premises: &[ProofExpr]) -> ConflictReport

Detect whether premises are jointly inconsistent, returning a kernel-checked proof of False and the indices of the clashing premises.

This is verified conflict detection: where an SMT-only tool returns “unsat”, this returns a certificate anyone can re-check, plus which rules conflict. A consistent rule set yields inconsistent == false with no proof — no false alarms.