// #TestSpec: redundant:req1; results:-1
Input x IS int
Input P IS bool
Input R IS bool

req1: Globally, it is always the case that "!R" holds
req2: Globally, it is always the case that "!R && P" holds