Function unit_propagate 

pub fn unit_propagate(clauses: &CanonClauses) -> CanonClauses

Unit-propagate a clause set to fixpoint: repeatedly assign a unit clause’s literal (drop satisfied clauses, delete the falsified literal), stopping at a derived ⊥ or when no unit remains. A sound structural reduction (RUP-certified), monotone under relabeling.