D-notation
Since a given major premise and a given minor premise uniquely determine the conclusion (up to variable renaming), Meredith observed that it was only necessary to note which two statements were involved and that the condensed detachment can be used without any other notation required. This led to the "D-notation" for proofs. This notation uses the "D" operator to mean condensed detachment, and takes 2 arguments, in a standard prefix notation string. For example, if you have four axioms a typical proof in D-notation might look like: DD12D34 which shows a condensed detachment step using the result of two prior condensed detachment steps, the first of which used axioms 1 and 2, and the second of which used axioms 3 and 4.
This notation, besides being used in some automated theorem provers, sometimes appears in catalogs of proofs
Condensed detachment's use of unification predates the resolution techniques of automated theorem proving.
Read more about this topic: Condensed Detachment