Description: A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018)