Using three values (0,1,X), N-input NAND requires N+1 vectors to verify
Hardware Verification - Application of formal techniques to chip designs Jacob Abraham (July 7, 2001)