U. Petermann, “On the practical value of Herbrand disjunctions”, LLP, vol. 8, no. 8, pp. 153–180, Jan. 2004.