Because of the complexity of digital system validation, formal verification has become an important member of the EDA tools. In formal verification, counterexamples help identify design problems and debugging. Almost all existing verification tools generate one counterexample when a property fails. This paper investigates, how debugging can benefit from using more than one counter-example generated by the verification tool. A new method for making counterexample is proposed that is based on PIRE (Property Intermediate Representation with Extensibility) structure. In this method, all possible counterexamples are generated.