Translating pure literal elimination into rup
Pure literal elimination over base clauses is effectively deleting those clauses from the formula, an action which cannot be encoded in a RUP proof since such proofs only encode clause additions.  But since an unsatisfiable formula will be unsatisfiable even without the clauses that contain pure literals you can treat the formula as if those clauses were not present.  Any RUP proof of the unsatisfiability of the formula with those clauses missing will also be a RUP proof of the unsatisfiability of the original formula.
As for the second example, you can't validly add $(\lnot A \lor \lnot B)$ to the proof because that clause isn't an actual requirement to satisfy the formula.  $A$ dominating $B$ after a partial assignment doesn't indicate that $\lnot B$ is mandatory, rather it means that asserting $B$ isn't helpful.  In fact, it might be a bad thing to do if $\lnot B$ is needed to satisfy some clauses later.  If you assert $\lnot B$ to satisfy all clauses containing $\lnot B$ you can be confident that $B$ will never appear in a downstream conflict clause and thus will never be part of a RUP clause generated by this partial assignment.  So asserting $\lnot B$ can't hurt but you can't be sure that it is necessary.  RUP proof clauses state only what is necessary.