Reverse Unit Propagation RUP proofs are a sequence of clauses that are redundant with respect to the input formula. To check that a clause C is redundant, all literals C are assigned to false followed by unit propagation. In order to verify redundancy, unit propagation should result in a conflict.

$ \curvearrowright$ Konflikt für F∧¬C $ \curvearrowright$ F∧¬C ist nicht erfüllbar $ \curvearrowright$ ¬FC ist allgemeingültig $ \curvearrowright$ F $ \models$ C (aus F folgt C) $ \curvearrowright$ C „ist redundant``

siehe auch E.Goldberg, Y.Novikov. Verification of proofs of unsatisfiability for CNF formulas. Design, Automation and Test in Europe. 2003, March 3-7,pp.886-891