Indrzejczak, A. Tautology Elimination, Cut Elimination, and S5. LLP 2017, 26, 461-471.