add Peirce's law as a test case of Tseitin encoding