S. Riis and M. Sitharam, “Generating Hard Tautologies Using Predicate Logic and the Symmetric Group”, BRICS, vol. 5, no. 19, Jan. 1998.