Given a set of disjunctions in propositional logic, they can be said to entail another disjunction D if the negation of D, when added as a set of unit clauses to the original set, yields an unsatisfiable formula.
One simple way to check unsatisfiablility is to perform iterated unit propagation on the new formula, and if a conflict emerges we can say the new clause is entailed. Clauses that can be immediately shown to be entailed using this "reverse unit propagation" (RUP) method are called asymmetric tautologies (AT).
As a logical inference system, AT is sound and complete, and generalizes both resolution and subsumption. Hence, it is a Frege system.
My question: is there any published literature on the strength of AT proofs? Are exponential lower time bounds known? Why are DRAT or RAT proofs used more often?