use plaisted instead of tseitin