// #TestSpec: rt-inconsistent:req1; vacuous:; inconsistent:; results: 4
Input a is bool
Input b is bool
Input c is bool
Input x is bool

req1: Globally, it is always the case that if "c" holds, then "a" holds after at most "50" time units
req2: Globally, it is always the case that if "c" holds, then "b" holds after at most "50" time units
//req3: Globally, it is never the case that "a" holds.
req3: Globally, it is always the case that if "x" holds, then "!a" holds as well.

// Requirements req2, req1 are rt-inconsistent
// We found a FailurePath: 
// INITIAL     a=* b=* c=*
// [0;50]      a=false b=true c=true

// actual rt-inconsistency should be just req1