// #TestSpec: redundant:req1; results: -1
input A is bool
input B is bool
input C is bool

req1: Globally, it is always the case that if "A" holds, then "B" holds as well
req2: Globally, it is always the case that if "A" holds, then "B && C" holds as well